GT000D

euclidean_trace_prefix_gcd_invariant

Natural induction over every actual beta-coded Euclidean transition preserves the gcd of the initial zero-divisor state at every history prefix.

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. ∀ s. ∀ h. ∀ e. ∀ l. ∀ g. ContinuedFractionTrace(a,b,s,h,e,l) → EuclideanStateAt(h,e,0,g,0,0) → ∀ x. Le(x,l) → ∃ y. ∃ z. ∃ n. EuclideanStateAt(h,e,x,y,z,n) ∧ IsGCD(g,y,z)

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

Definition DAG

ContinuedFractionTrace(a,b,s,u,v,ell) · 1EuclideanStateAt(h,s,i,a,b,q) · 2Le(a,b) · 1IsGCD(g,a,b) · 1

Actual proof prerequisites

euclidean_beta_state_functionalis_gcd_zero_right · checked external prerequisitelt_to_le · checked external prerequisiteis_gcd_euclid_forward · checked external prerequisite
Original expanded first-order statement 
forall a b s h e l g. (exists cf_gcd_egt_trace. ((((exists ff_h_cf_egt_trace_initial_state. ff_h_cf_egt_trace_initial_state + S (((cf_gcd_egt_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_egt_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_trace_initial_state. h = ff_q_cf_egt_trace_initial_state * S ((S (0)) * e) + (((cf_gcd_egt_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_egt_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_trace_terminal_state. ff_h_cf_egt_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 (l)) * e)) /\ exists ff_q_cf_egt_trace_terminal_state. h = ff_q_cf_egt_trace_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_trace. (exists ff_lt_cf_egt_trace_index. ff_lt_cf_egt_trace_index + S cf_index_egt_trace = l) -> exists cf_old_a_egt_trace cf_old_b_egt_trace cf_tail_egt_trace cf_new_a_egt_trace cf_new_b_egt_trace cf_head_egt_trace cf_quotient_egt_trace. ((((exists ff_h_cf_egt_trace_previous_state. ff_h_cf_egt_trace_previous_state + S (((cf_old_a_egt_trace) + (((cf_old_b_egt_trace) + (cf_tail_egt_trace)) * S ((cf_old_b_egt_trace) + (cf_tail_egt_trace)) + ((cf_tail_egt_trace) + (cf_tail_egt_trace)))) * S ((cf_old_a_egt_trace) + (((cf_old_b_egt_trace) + (cf_tail_egt_trace)) * S ((cf_old_b_egt_trace) + (cf_tail_egt_trace)) + ((cf_tail_egt_trace) + (cf_tail_egt_trace)))) + ((((cf_old_b_egt_trace) + (cf_tail_egt_trace)) * S ((cf_old_b_egt_trace) + (cf_tail_egt_trace)) + ((cf_tail_egt_trace) + (cf_tail_egt_trace))) + (((cf_old_b_egt_trace) + (cf_tail_egt_trace)) * S ((cf_old_b_egt_trace) + (cf_tail_egt_trace)) + ((cf_tail_egt_trace) + (cf_tail_egt_trace))))) = S ((S (cf_index_egt_trace)) * e)) /\ exists ff_q_cf_egt_trace_previous_state. h = ff_q_cf_egt_trace_previous_state * S ((S (cf_index_egt_trace)) * e) + (((cf_old_a_egt_trace) + (((cf_old_b_egt_trace) + (cf_tail_egt_trace)) * S ((cf_old_b_egt_trace) + (cf_tail_egt_trace)) + ((cf_tail_egt_trace) + (cf_tail_egt_trace)))) * S ((cf_old_a_egt_trace) + (((cf_old_b_egt_trace) + (cf_tail_egt_trace)) * S ((cf_old_b_egt_trace) + (cf_tail_egt_trace)) + ((cf_tail_egt_trace) + (cf_tail_egt_trace)))) + ((((cf_old_b_egt_trace) + (cf_tail_egt_trace)) * S ((cf_old_b_egt_trace) + (cf_tail_egt_trace)) + ((cf_tail_egt_trace) + (cf_tail_egt_trace))) + (((cf_old_b_egt_trace) + (cf_tail_egt_trace)) * S ((cf_old_b_egt_trace) + (cf_tail_egt_trace)) + ((cf_tail_egt_trace) + (cf_tail_egt_trace))))))) /\ ((((exists ff_h_cf_egt_trace_following_state. ff_h_cf_egt_trace_following_state + S (((cf_new_a_egt_trace) + (((cf_new_b_egt_trace) + (cf_head_egt_trace)) * S ((cf_new_b_egt_trace) + (cf_head_egt_trace)) + ((cf_head_egt_trace) + (cf_head_egt_trace)))) * S ((cf_new_a_egt_trace) + (((cf_new_b_egt_trace) + (cf_head_egt_trace)) * S ((cf_new_b_egt_trace) + (cf_head_egt_trace)) + ((cf_head_egt_trace) + (cf_head_egt_trace)))) + ((((cf_new_b_egt_trace) + (cf_head_egt_trace)) * S ((cf_new_b_egt_trace) + (cf_head_egt_trace)) + ((cf_head_egt_trace) + (cf_head_egt_trace))) + (((cf_new_b_egt_trace) + (cf_head_egt_trace)) * S ((cf_new_b_egt_trace) + (cf_head_egt_trace)) + ((cf_head_egt_trace) + (cf_head_egt_trace))))) = S ((S (S cf_index_egt_trace)) * e)) /\ exists ff_q_cf_egt_trace_following_state. h = ff_q_cf_egt_trace_following_state * S ((S (S cf_index_egt_trace)) * e) + (((cf_new_a_egt_trace) + (((cf_new_b_egt_trace) + (cf_head_egt_trace)) * S ((cf_new_b_egt_trace) + (cf_head_egt_trace)) + ((cf_head_egt_trace) + (cf_head_egt_trace)))) * S ((cf_new_a_egt_trace) + (((cf_new_b_egt_trace) + (cf_head_egt_trace)) * S ((cf_new_b_egt_trace) + (cf_head_egt_trace)) + ((cf_head_egt_trace) + (cf_head_egt_trace)))) + ((((cf_new_b_egt_trace) + (cf_head_egt_trace)) * S ((cf_new_b_egt_trace) + (cf_head_egt_trace)) + ((cf_head_egt_trace) + (cf_head_egt_trace))) + (((cf_new_b_egt_trace) + (cf_head_egt_trace)) * S ((cf_new_b_egt_trace) + (cf_head_egt_trace)) + ((cf_head_egt_trace) + (cf_head_egt_trace))))))) /\ (cf_new_b_egt_trace = cf_old_a_egt_trace /\ (cf_new_a_egt_trace = cf_new_b_egt_trace * cf_quotient_egt_trace + cf_old_b_egt_trace /\ ((exists ff_lt_cf_egt_trace_remainder. ff_lt_cf_egt_trace_remainder + S cf_old_b_egt_trace = cf_new_b_egt_trace) /\ (cf_head_egt_trace = S ((cf_quotient_egt_trace + cf_tail_egt_trace) * S (cf_quotient_egt_trace + cf_tail_egt_trace) + (cf_tail_egt_trace + cf_tail_egt_trace))))))))))) -> (((exists ff_h_cf_egt_start_state. ff_h_cf_egt_start_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_start_state. h = ff_q_cf_egt_start_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))))))) -> forall i. (exists gap. gap + i = l) -> (exists egt_left_at egt_right_at egt_list_at. ((((exists ff_h_cf_egt_at_state_state. ff_h_cf_egt_at_state_state + S (((egt_left_at) + (((egt_right_at) + (egt_list_at)) * S ((egt_right_at) + (egt_list_at)) + ((egt_list_at) + (egt_list_at)))) * S ((egt_left_at) + (((egt_right_at) + (egt_list_at)) * S ((egt_right_at) + (egt_list_at)) + ((egt_list_at) + (egt_list_at)))) + ((((egt_right_at) + (egt_list_at)) * S ((egt_right_at) + (egt_list_at)) + ((egt_list_at) + (egt_list_at))) + (((egt_right_at) + (egt_list_at)) * S ((egt_right_at) + (egt_list_at)) + ((egt_list_at) + (egt_list_at))))) = S ((S (i)) * e)) /\ exists ff_q_cf_egt_at_state_state. h = ff_q_cf_egt_at_state_state * S ((S (i)) * e) + (((egt_left_at) + (((egt_right_at) + (egt_list_at)) * S ((egt_right_at) + (egt_list_at)) + ((egt_list_at) + (egt_list_at)))) * S ((egt_left_at) + (((egt_right_at) + (egt_list_at)) * S ((egt_right_at) + (egt_list_at)) + ((egt_list_at) + (egt_list_at)))) + ((((egt_right_at) + (egt_list_at)) * S ((egt_right_at) + (egt_list_at)) + ((egt_list_at) + (egt_list_at))) + (((egt_right_at) + (egt_list_at)) * S ((egt_right_at) + (egt_list_at)) + ((egt_list_at) + (egt_list_at))))))) /\ ((((exists ec_gcd_left_egt_at_gcd. egt_left_at = g * ec_gcd_left_egt_at_gcd) /\ (exists ec_gcd_right_egt_at_gcd. egt_right_at = g * ec_gcd_right_egt_at_gcd)) /\ forall ec_gcd_common_egt_at_gcd. (exists ec_gcd_common_left_egt_at_gcd. egt_left_at = ec_gcd_common_egt_at_gcd * ec_gcd_common_left_egt_at_gcd) -> (exists ec_gcd_common_right_egt_at_gcd. egt_right_at = ec_gcd_common_egt_at_gcd * ec_gcd_common_right_egt_at_gcd) -> exists ec_gcd_greatest_egt_at_gcd. g = ec_gcd_common_egt_at_gcd * ec_gcd_greatest_egt_at_gcd))))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

84 script commands · 23 reading checkpoints · 4 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 beta state functional

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

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro s
  4. L4
    intro h
  5. L5
    intro e
  6. L6
    intro l
  7. L7
    intro g
  8. L8
    intro htrace
  9. L9
    intro hstart
02Separate the logical casesL10–12

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

  1. L10
    cases htrace
  2. L11
    cases htrace_witness
  3. L12
    cases htrace_witness_right
03Fix variables and assumptionsL13–13

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

  1. L13
    intro i
04Induction on iL14–15

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L14
    induction i
  2. L15
    intro hbound
05Construct an explicit witnessL16–18

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

  1. L16
    exists g
  2. L17
    exists 0
  3. L18
    exists 0
06Separate the logical casesL19–19

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

  1. L19
    split
07Use earlier factsL20–22

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

  1. L20
    exact hstart
  2. L21
    specialize is_gcd_zero_right g
  3. L22
    exact is_gcd_zero_right
08Fix variables and assumptionsL23–23

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

  1. L23
    intro hbound
09Establish hprevboundL24–28

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lt to le.

  1. L24
    have hprevbound : exists gap. gap + i = l
  2. L25
    specialize lt_to_le i
  3. L26
    specialize lt_to_le l
  4. L27
    apply lt_to_le
  5. L28
    exact hbound
10Establish hpreviousL29–31

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

  1. L29
    have hprevious : ∃ egt_left_previous. ∃ egt_right_previous. ∃ egt_list_previous. EuclideanStateAt(h,e,i,egt_left_previous,egt_right_previous,egt_list_previous) ∧ IsGCD(g,egt_left_previous,egt_right_previous)Definitions: EuclideanStateAtIsGCDOriginal native command in the exact edition
  2. L30
    apply IH
  3. L31
    exact hprevbound
11Separate the logical casesL32–35

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

  1. L32
    cases hprevious
  2. L33
    cases hprevious_witness
  3. L34
    cases hprevious_witness_witness
  4. L35
    cases hprevious_witness_witness_witness
12Establish htransitionL36–39

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply htrace witness right right.

  1. L36
    have htransition · expand full local formula (636 characters)have htransition : ∃ egt_old_a_induction. ∃ egt_old_b_induction. ∃ egt_old_list_induction. ∃ egt_new_a_induction. ∃ egt_new_b_induction. ∃ egt_new_list_induction. ∃ egt_quotient_induction. EuclideanStateAt(h,e,i,egt_old_a_induction,egt_old_b_induction,egt_old_list_induction) ∧ (EuclideanStateAt(h,e,S i,egt_new_a_induction,egt_new_b_induction,egt_new_list_induction) ∧ (egt_new_b_induction = egt_old_a_induction ∧ (egt_new_a_induction = egt_new_b_induction · egt_quotient_induction + egt_old_b_induction ∧ (Lt(egt_old_b_induction,egt_new_b_induction) ∧ ListCell(egt_new_list_induction,egt_quotient_induction,egt_old_list_induction)))))
    Definitions: ListCellEuclideanStateAtLtOriginal native command in the exact edition
  2. L37
    specialize htrace_witness_right_right i
  3. L38
    apply htrace_witness_right_right
  4. L39
    exact hbound
13Separate the logical casesL40–49

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

  1. L40
    cases htransition
  2. L41
    cases htransition_witness
  3. L42
    cases htransition_witness_witness
  4. L43
    cases htransition_witness_witness_witness
  5. L44
    cases htransition_witness_witness_witness_witness
  6. L45
    cases htransition_witness_witness_witness_witness_witness
  7. L46
    cases htransition_witness_witness_witness_witness_witness_witness
  8. L47
    cases htransition_witness_witness_witness_witness_witness_witness_witness
  9. L48
    cases htransition_witness_witness_witness_witness_witness_witness_witness_right
  10. L49
    cases htransition_witness_witness_witness_witness_witness_witness_witness_right_right
14Separate the logical casesL50–50

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

  1. L50
    cases htransition_witness_witness_witness_witness_witness_witness_witness_right_right_right
15Establish halignL51–60

Establish this local claim before using it. It is not an additional assumption.

  1. L51
    have halign : x1 = x4 /\ (x2 = x5 /\ x3 = x6)
  2. L52
    specialize euclidean_beta_state_functional h
  3. L53
    specialize euclidean_beta_state_functional e
  4. L54
    specialize euclidean_beta_state_functional i
  5. L55
    specialize euclidean_beta_state_functional x1
  6. L56
    specialize euclidean_beta_state_functional x2
  7. L57
    specialize euclidean_beta_state_functional x3
  8. L58
    specialize euclidean_beta_state_functional x4
  9. L59
    specialize euclidean_beta_state_functional x5
  10. L60
    specialize euclidean_beta_state_functional x6
16Use earlier factsL61–63

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

  1. L61
    apply euclidean_beta_state_functional
  2. L62
    exact hprevious_witness_witness_witness_left
  3. L63
    exact htransition_witness_witness_witness_witness_witness_witness_witness_left
17Separate the logical casesL64–65

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

  1. L64
    cases halign
  2. L65
    cases halign_right
18Calculate and transport equalitiesL66–69

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

  1. L66
    rewrite halign_left at hprevious_witness_witness_witness_right
  2. L67
    rewrite halign_left at hprevious_witness_witness_witness_right
  3. L68
    rewrite halign_right_left at hprevious_witness_witness_witness_right
  4. L69
    rewrite halign_right_left at hprevious_witness_witness_witness_right
19Construct an explicit witnessL70–72

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

  1. L70
    exists x7
  2. L71
    exists x8
  3. L72
    exists x9
20Separate the logical casesL73–73

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

  1. L73
    split
21Use earlier factsL74–81

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

  1. L74
    exact htransition_witness_witness_witness_witness_witness_witness_witness_right_left
  2. L75
    specialize is_gcd_euclid_forward g
  3. L76
    specialize is_gcd_euclid_forward x7
  4. L77
    specialize is_gcd_euclid_forward x8
  5. L78
    specialize is_gcd_euclid_forward x10
  6. L79
    specialize is_gcd_euclid_forward x5
  7. L80
    apply is_gcd_euclid_forward
  8. L81
    exact htransition_witness_witness_witness_witness_witness_witness_witness_right_right_right_left
22Calculate and transport equalitiesL82–83

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

  1. L82
    rewrite htransition_witness_witness_witness_witness_witness_witness_witness_right_right_left
  2. L83
    rewrite htransition_witness_witness_witness_witness_witness_witness_witness_right_right_left
23Use earlier factsL84–84

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

  1. L84
    exact hprevious_witness_witness_witness_right

Library-wide reading audit

Original defined command ledger · 84 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro s
  4. 0004intro h
  5. 0005intro e
  6. 0006intro l
  7. 0007intro g
  8. 0008intro htrace
  9. 0009intro hstart
  10. 0010cases htrace
  11. 0011cases htrace_witness
  12. 0012cases htrace_witness_right
  13. 0013intro i
  14. 0014induction i
  15. 0015intro hbound
  16. 0016exists g
  17. 0017exists 0
  18. 0018exists 0
  19. 0019split
  20. 0020exact hstart
  21. 0021specialize is_gcd_zero_right g
  22. 0022exact is_gcd_zero_right
  23. 0023intro hbound
  24. 0024have hprevbound : exists gap. gap + i = l
  25. 0025specialize lt_to_le i
  26. 0026specialize lt_to_le l
  27. 0027apply lt_to_le
  28. 0028exact hbound
  29. 0029have hprevious : exists egt_left_previous egt_right_previous egt_list_previous. ((((exists ff_h_cf_egt_previous_state_state. ff_h_cf_egt_previous_state_state + S (((egt_left_previous) + (((egt_right_previous) + (egt_list_previous)) * S ((egt_right_previous) + (egt_list_previous)) + ((egt_list_previous) + (egt_list_previous)))) * S ((egt_left_previous) + (((egt_right_previous) + (egt_list_previous)) * S ((egt_right_previous) + (egt_list_previous)) + ((egt_list_previous) + (egt_list_previous)))) + ((((egt_right_previous) + (egt_list_previous)) * S ((egt_right_previous) + (egt_list_previous)) + ((egt_list_previous) + (egt_list_previous))) + (((egt_right_previous) + (egt_list_previous)) * S ((egt_right_previous) + (egt_list_previous)) + ((egt_list_previous) + (egt_list_previous))))) = S ((S (i)) * e)) /\ exists ff_q_cf_egt_previous_state_state. h = ff_q_cf_egt_previous_state_state * S ((S (i)) * e) + (((egt_left_previous) + (((egt_right_previous) + (egt_list_previous)) * S ((egt_right_previous) + (egt_list_previous)) + ((egt_list_previous) + (egt_list_previous)))) * S ((egt_left_previous) + (((egt_right_previous) + (egt_list_previous)) * S ((egt_right_previous) + (egt_list_previous)) + ((egt_list_previous) + (egt_list_previous)))) + ((((egt_right_previous) + (egt_list_previous)) * S ((egt_right_previous) + (egt_list_previous)) + ((egt_list_previous) + (egt_list_previous))) + (((egt_right_previous) + (egt_list_previous)) * S ((egt_right_previous) + (egt_list_previous)) + ((egt_list_previous) + (egt_list_previous))))))) /\ ((((exists ec_gcd_left_egt_previous_gcd. egt_left_previous = g * ec_gcd_left_egt_previous_gcd) /\ (exists ec_gcd_right_egt_previous_gcd. egt_right_previous = g * ec_gcd_right_egt_previous_gcd)) /\ forall ec_gcd_common_egt_previous_gcd. (exists ec_gcd_common_left_egt_previous_gcd. egt_left_previous = ec_gcd_common_egt_previous_gcd * ec_gcd_common_left_egt_previous_gcd) -> (exists ec_gcd_common_right_egt_previous_gcd. egt_right_previous = ec_gcd_common_egt_previous_gcd * ec_gcd_common_right_egt_previous_gcd) -> exists ec_gcd_greatest_egt_previous_gcd. g = ec_gcd_common_egt_previous_gcd * ec_gcd_greatest_egt_previous_gcd)))
  30. 0030apply IH
  31. 0031exact hprevbound
  32. 0032cases hprevious
  33. 0033cases hprevious_witness
  34. 0034cases hprevious_witness_witness
  35. 0035cases hprevious_witness_witness_witness
  36. 0036have htransition : exists egt_old_a_induction egt_old_b_induction egt_old_list_induction egt_new_a_induction egt_new_b_induction egt_new_list_induction egt_quotient_induction. ((((exists ff_h_cf_egt_induction_previous_state. ff_h_cf_egt_induction_previous_state + S (((egt_old_a_induction) + (((egt_old_b_induction) + (egt_old_list_induction)) * S ((egt_old_b_induction) + (egt_old_list_induction)) + ((egt_old_list_induction) + (egt_old_list_induction)))) * S ((egt_old_a_induction) + (((egt_old_b_induction) + (egt_old_list_induction)) * S ((egt_old_b_induction) + (egt_old_list_induction)) + ((egt_old_list_induction) + (egt_old_list_induction)))) + ((((egt_old_b_induction) + (egt_old_list_induction)) * S ((egt_old_b_induction) + (egt_old_list_induction)) + ((egt_old_list_induction) + (egt_old_list_induction))) + (((egt_old_b_induction) + (egt_old_list_induction)) * S ((egt_old_b_induction) + (egt_old_list_induction)) + ((egt_old_list_induction) + (egt_old_list_induction))))) = S ((S (i)) * e)) /\ exists ff_q_cf_egt_induction_previous_state. h = ff_q_cf_egt_induction_previous_state * S ((S (i)) * e) + (((egt_old_a_induction) + (((egt_old_b_induction) + (egt_old_list_induction)) * S ((egt_old_b_induction) + (egt_old_list_induction)) + ((egt_old_list_induction) + (egt_old_list_induction)))) * S ((egt_old_a_induction) + (((egt_old_b_induction) + (egt_old_list_induction)) * S ((egt_old_b_induction) + (egt_old_list_induction)) + ((egt_old_list_induction) + (egt_old_list_induction)))) + ((((egt_old_b_induction) + (egt_old_list_induction)) * S ((egt_old_b_induction) + (egt_old_list_induction)) + ((egt_old_list_induction) + (egt_old_list_induction))) + (((egt_old_b_induction) + (egt_old_list_induction)) * S ((egt_old_b_induction) + (egt_old_list_induction)) + ((egt_old_list_induction) + (egt_old_list_induction))))))) /\ ((((exists ff_h_cf_egt_induction_following_state. ff_h_cf_egt_induction_following_state + S (((egt_new_a_induction) + (((egt_new_b_induction) + (egt_new_list_induction)) * S ((egt_new_b_induction) + (egt_new_list_induction)) + ((egt_new_list_induction) + (egt_new_list_induction)))) * S ((egt_new_a_induction) + (((egt_new_b_induction) + (egt_new_list_induction)) * S ((egt_new_b_induction) + (egt_new_list_induction)) + ((egt_new_list_induction) + (egt_new_list_induction)))) + ((((egt_new_b_induction) + (egt_new_list_induction)) * S ((egt_new_b_induction) + (egt_new_list_induction)) + ((egt_new_list_induction) + (egt_new_list_induction))) + (((egt_new_b_induction) + (egt_new_list_induction)) * S ((egt_new_b_induction) + (egt_new_list_induction)) + ((egt_new_list_induction) + (egt_new_list_induction))))) = S ((S (S i)) * e)) /\ exists ff_q_cf_egt_induction_following_state. h = ff_q_cf_egt_induction_following_state * S ((S (S i)) * e) + (((egt_new_a_induction) + (((egt_new_b_induction) + (egt_new_list_induction)) * S ((egt_new_b_induction) + (egt_new_list_induction)) + ((egt_new_list_induction) + (egt_new_list_induction)))) * S ((egt_new_a_induction) + (((egt_new_b_induction) + (egt_new_list_induction)) * S ((egt_new_b_induction) + (egt_new_list_induction)) + ((egt_new_list_induction) + (egt_new_list_induction)))) + ((((egt_new_b_induction) + (egt_new_list_induction)) * S ((egt_new_b_induction) + (egt_new_list_induction)) + ((egt_new_list_induction) + (egt_new_list_induction))) + (((egt_new_b_induction) + (egt_new_list_induction)) * S ((egt_new_b_induction) + (egt_new_list_induction)) + ((egt_new_list_induction) + (egt_new_list_induction))))))) /\ (egt_new_b_induction = egt_old_a_induction /\ (egt_new_a_induction = egt_new_b_induction * egt_quotient_induction + egt_old_b_induction /\ ((exists ff_lt_egt_induction_remainder. ff_lt_egt_induction_remainder + S egt_old_b_induction = egt_new_b_induction) /\ (egt_new_list_induction = S ((egt_quotient_induction + egt_old_list_induction) * S (egt_quotient_induction + egt_old_list_induction) + (egt_old_list_induction + egt_old_list_induction))))))))
  37. 0037specialize htrace_witness_right_right i
  38. 0038apply htrace_witness_right_right
  39. 0039exact hbound
  40. 0040cases htransition
  41. 0041cases htransition_witness
  42. 0042cases htransition_witness_witness
  43. 0043cases htransition_witness_witness_witness
  44. 0044cases htransition_witness_witness_witness_witness
  45. 0045cases htransition_witness_witness_witness_witness_witness
  46. 0046cases htransition_witness_witness_witness_witness_witness_witness
  47. 0047cases htransition_witness_witness_witness_witness_witness_witness_witness
  48. 0048cases htransition_witness_witness_witness_witness_witness_witness_witness_right
  49. 0049cases htransition_witness_witness_witness_witness_witness_witness_witness_right_right
  50. 0050cases htransition_witness_witness_witness_witness_witness_witness_witness_right_right_right
  51. 0051have halign : x1 = x4 /\ (x2 = x5 /\ x3 = x6)
  52. 0052specialize euclidean_beta_state_functional h
  53. 0053specialize euclidean_beta_state_functional e
  54. 0054specialize euclidean_beta_state_functional i
  55. 0055specialize euclidean_beta_state_functional x1
  56. 0056specialize euclidean_beta_state_functional x2
  57. 0057specialize euclidean_beta_state_functional x3
  58. 0058specialize euclidean_beta_state_functional x4
  59. 0059specialize euclidean_beta_state_functional x5
  60. 0060specialize euclidean_beta_state_functional x6
  61. 0061apply euclidean_beta_state_functional
  62. 0062exact hprevious_witness_witness_witness_left
  63. 0063exact htransition_witness_witness_witness_witness_witness_witness_witness_left
  64. 0064cases halign
  65. 0065cases halign_right
  66. 0066rewrite halign_left at hprevious_witness_witness_witness_right
  67. 0067rewrite halign_left at hprevious_witness_witness_witness_right
  68. 0068rewrite halign_right_left at hprevious_witness_witness_witness_right
  69. 0069rewrite halign_right_left at hprevious_witness_witness_witness_right
  70. 0070exists x7
  71. 0071exists x8
  72. 0072exists x9
  73. 0073split
  74. 0074exact htransition_witness_witness_witness_witness_witness_witness_witness_right_left
  75. 0075specialize is_gcd_euclid_forward g
  76. 0076specialize is_gcd_euclid_forward x7
  77. 0077specialize is_gcd_euclid_forward x8
  78. 0078specialize is_gcd_euclid_forward x10
  79. 0079specialize is_gcd_euclid_forward x5
  80. 0080apply is_gcd_euclid_forward
  81. 0081exact htransition_witness_witness_witness_witness_witness_witness_witness_right_right_right_left
  82. 0082rewrite htransition_witness_witness_witness_witness_witness_witness_witness_right_right_left
  83. 0083rewrite htransition_witness_witness_witness_witness_witness_witness_witness_right_right_left
  84. 0084exact hprevious_witness_witness_witness_right