EL000C

euclidean_log_trace_below_power

Induction on a witnessed power of two constructs genuine complete Euclidean beta histories in at most twice the exponent, using strict halving across every actual pair of divisions.

Alpha v34 checked-use · first admitted v23 · 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.

The exact G101 milestone is fully proved, including the stronger checked bound k≤2·BitLen(b), a real beta-coded execution, and its actual terminal gcd. The independent T13 determinant/rank/integer-span substrate is now closed in the separate Alpha-v27 integer-linear-algebra branch. Full T13 proof · Alpha v27

Exact theorem in conservative defined notation

∀ n. ∀ p. PowTwo(n,p) → ∀ x. Lt(x,p) → ∀ y. EuclideanBoundedTrace(y,x,n + n)

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

Definition DAG

PowTwo(e,p) · 1EuclideanBoundedTrace(a,b,B) · 1Lt(a,b) · 1

Actual proof prerequisites

euclidean_log_power_zero_divisoreuclidean_log_budget_zero_divisorbinary_power_two_exists · checked external prerequisitebinary_power_two_successor_double · checked external prerequisiteeq_decidable · checked external prerequisiteeuclidean_division_step_exists · checked external prerequisitezero_or_succ · checked external prerequisiteeuclidean_log_budget_extendeuclidean_log_budget_weakeneuclidean_log_budget_successor_powerdivision_remainder_exists · checked external prerequisiteeuclidean_two_step_halving · checked external prerequisiteeuclidean_log_halving_power_dropeuclidean_log_budget_extend_twice
Original expanded first-order statement 
forall n p. (exists pa_b_bl_elb_power pa_c_bl_elb_power. ((forall pa_i_bl_elb_power_repeat. (exists pa_lt_bl_elb_power_repeat_bound. pa_lt_bl_elb_power_repeat_bound + S pa_i_bl_elb_power_repeat = n) -> (((exists pa_h_bl_elb_power_repeat_decoded. pa_h_bl_elb_power_repeat_decoded + S (2) = S ((S (pa_i_bl_elb_power_repeat)) * pa_c_bl_elb_power)) /\ exists pa_q_bl_elb_power_repeat_decoded. pa_b_bl_elb_power = pa_q_bl_elb_power_repeat_decoded * S ((S (pa_i_bl_elb_power_repeat)) * pa_c_bl_elb_power) + (2)))) /\ (exists pa_u_bl_elb_power_product pa_v_bl_elb_power_product. ((((exists pa_h_bl_elb_power_product_start. pa_h_bl_elb_power_product_start + S (1) = S ((S (0)) * pa_v_bl_elb_power_product)) /\ exists pa_q_bl_elb_power_product_start. pa_u_bl_elb_power_product = pa_q_bl_elb_power_product_start * S ((S (0)) * pa_v_bl_elb_power_product) + (1))) /\ ((((exists pa_h_bl_elb_power_product_terminal. pa_h_bl_elb_power_product_terminal + S (p) = S ((S (n)) * pa_v_bl_elb_power_product)) /\ exists pa_q_bl_elb_power_product_terminal. pa_u_bl_elb_power_product = pa_q_bl_elb_power_product_terminal * S ((S (n)) * pa_v_bl_elb_power_product) + (p))) /\ forall pa_i_bl_elb_power_product. (exists pa_lt_bl_elb_power_product_bound. pa_lt_bl_elb_power_product_bound + S pa_i_bl_elb_power_product = n) -> exists pa_p_bl_elb_power_product pa_r_bl_elb_power_product pa_s_bl_elb_power_product. ((((exists pa_h_bl_elb_power_product_factor. pa_h_bl_elb_power_product_factor + S (pa_p_bl_elb_power_product) = S ((S (pa_i_bl_elb_power_product)) * pa_c_bl_elb_power)) /\ exists pa_q_bl_elb_power_product_factor. pa_b_bl_elb_power = pa_q_bl_elb_power_product_factor * S ((S (pa_i_bl_elb_power_product)) * pa_c_bl_elb_power) + (pa_p_bl_elb_power_product))) /\ ((((exists pa_h_bl_elb_power_product_partial. pa_h_bl_elb_power_product_partial + S (pa_r_bl_elb_power_product) = S ((S (pa_i_bl_elb_power_product)) * pa_v_bl_elb_power_product)) /\ exists pa_q_bl_elb_power_product_partial. pa_u_bl_elb_power_product = pa_q_bl_elb_power_product_partial * S ((S (pa_i_bl_elb_power_product)) * pa_v_bl_elb_power_product) + (pa_r_bl_elb_power_product))) /\ ((((exists pa_h_bl_elb_power_product_successor. pa_h_bl_elb_power_product_successor + S (pa_s_bl_elb_power_product) = S ((S (S pa_i_bl_elb_power_product)) * pa_v_bl_elb_power_product)) /\ exists pa_q_bl_elb_power_product_successor. pa_u_bl_elb_power_product = pa_q_bl_elb_power_product_successor * S ((S (S pa_i_bl_elb_power_product)) * pa_v_bl_elb_power_product) + (pa_s_bl_elb_power_product))) /\ pa_s_bl_elb_power_product = pa_r_bl_elb_power_product * pa_p_bl_elb_power_product)))))))) -> forall b. (exists ff_lt_elb_below. ff_lt_elb_below + S b = p) -> forall a. (exists elb_list_induction elb_history_induction elb_scale_induction elb_steps_induction. ((exists cf_gcd_elb_induction_budget. ((((exists ff_h_cf_elb_induction_budget_initial_state. ff_h_cf_elb_induction_budget_initial_state + S (((cf_gcd_elb_induction_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_induction_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * elb_scale_induction)) /\ exists ff_q_cf_elb_induction_budget_initial_state. elb_history_induction = ff_q_cf_elb_induction_budget_initial_state * S ((S (0)) * elb_scale_induction) + (((cf_gcd_elb_induction_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_induction_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))))) /\ ((((exists ff_h_cf_elb_induction_budget_terminal_state. ff_h_cf_elb_induction_budget_terminal_state + S (((a) + (((b) + (elb_list_induction)) * S ((b) + (elb_list_induction)) + ((elb_list_induction) + (elb_list_induction)))) * S ((a) + (((b) + (elb_list_induction)) * S ((b) + (elb_list_induction)) + ((elb_list_induction) + (elb_list_induction)))) + ((((b) + (elb_list_induction)) * S ((b) + (elb_list_induction)) + ((elb_list_induction) + (elb_list_induction))) + (((b) + (elb_list_induction)) * S ((b) + (elb_list_induction)) + ((elb_list_induction) + (elb_list_induction))))) = S ((S (elb_steps_induction)) * elb_scale_induction)) /\ exists ff_q_cf_elb_induction_budget_terminal_state. elb_history_induction = ff_q_cf_elb_induction_budget_terminal_state * S ((S (elb_steps_induction)) * elb_scale_induction) + (((a) + (((b) + (elb_list_induction)) * S ((b) + (elb_list_induction)) + ((elb_list_induction) + (elb_list_induction)))) * S ((a) + (((b) + (elb_list_induction)) * S ((b) + (elb_list_induction)) + ((elb_list_induction) + (elb_list_induction)))) + ((((b) + (elb_list_induction)) * S ((b) + (elb_list_induction)) + ((elb_list_induction) + (elb_list_induction))) + (((b) + (elb_list_induction)) * S ((b) + (elb_list_induction)) + ((elb_list_induction) + (elb_list_induction))))))) /\ forall cf_index_elb_induction_budget. (exists ff_lt_cf_elb_induction_budget_index. ff_lt_cf_elb_induction_budget_index + S cf_index_elb_induction_budget = elb_steps_induction) -> exists cf_old_a_elb_induction_budget cf_old_b_elb_induction_budget cf_tail_elb_induction_budget cf_new_a_elb_induction_budget cf_new_b_elb_induction_budget cf_head_elb_induction_budget cf_quotient_elb_induction_budget. ((((exists ff_h_cf_elb_induction_budget_previous_state. ff_h_cf_elb_induction_budget_previous_state + S (((cf_old_a_elb_induction_budget) + (((cf_old_b_elb_induction_budget) + (cf_tail_elb_induction_budget)) * S ((cf_old_b_elb_induction_budget) + (cf_tail_elb_induction_budget)) + ((cf_tail_elb_induction_budget) + (cf_tail_elb_induction_budget)))) * S ((cf_old_a_elb_induction_budget) + (((cf_old_b_elb_induction_budget) + (cf_tail_elb_induction_budget)) * S ((cf_old_b_elb_induction_budget) + (cf_tail_elb_induction_budget)) + ((cf_tail_elb_induction_budget) + (cf_tail_elb_induction_budget)))) + ((((cf_old_b_elb_induction_budget) + (cf_tail_elb_induction_budget)) * S ((cf_old_b_elb_induction_budget) + (cf_tail_elb_induction_budget)) + ((cf_tail_elb_induction_budget) + (cf_tail_elb_induction_budget))) + (((cf_old_b_elb_induction_budget) + (cf_tail_elb_induction_budget)) * S ((cf_old_b_elb_induction_budget) + (cf_tail_elb_induction_budget)) + ((cf_tail_elb_induction_budget) + (cf_tail_elb_induction_budget))))) = S ((S (cf_index_elb_induction_budget)) * elb_scale_induction)) /\ exists ff_q_cf_elb_induction_budget_previous_state. elb_history_induction = ff_q_cf_elb_induction_budget_previous_state * S ((S (cf_index_elb_induction_budget)) * elb_scale_induction) + (((cf_old_a_elb_induction_budget) + (((cf_old_b_elb_induction_budget) + (cf_tail_elb_induction_budget)) * S ((cf_old_b_elb_induction_budget) + (cf_tail_elb_induction_budget)) + ((cf_tail_elb_induction_budget) + (cf_tail_elb_induction_budget)))) * S ((cf_old_a_elb_induction_budget) + (((cf_old_b_elb_induction_budget) + (cf_tail_elb_induction_budget)) * S ((cf_old_b_elb_induction_budget) + (cf_tail_elb_induction_budget)) + ((cf_tail_elb_induction_budget) + (cf_tail_elb_induction_budget)))) + ((((cf_old_b_elb_induction_budget) + (cf_tail_elb_induction_budget)) * S ((cf_old_b_elb_induction_budget) + (cf_tail_elb_induction_budget)) + ((cf_tail_elb_induction_budget) + (cf_tail_elb_induction_budget))) + (((cf_old_b_elb_induction_budget) + (cf_tail_elb_induction_budget)) * S ((cf_old_b_elb_induction_budget) + (cf_tail_elb_induction_budget)) + ((cf_tail_elb_induction_budget) + (cf_tail_elb_induction_budget))))))) /\ ((((exists ff_h_cf_elb_induction_budget_following_state. ff_h_cf_elb_induction_budget_following_state + S (((cf_new_a_elb_induction_budget) + (((cf_new_b_elb_induction_budget) + (cf_head_elb_induction_budget)) * S ((cf_new_b_elb_induction_budget) + (cf_head_elb_induction_budget)) + ((cf_head_elb_induction_budget) + (cf_head_elb_induction_budget)))) * S ((cf_new_a_elb_induction_budget) + (((cf_new_b_elb_induction_budget) + (cf_head_elb_induction_budget)) * S ((cf_new_b_elb_induction_budget) + (cf_head_elb_induction_budget)) + ((cf_head_elb_induction_budget) + (cf_head_elb_induction_budget)))) + ((((cf_new_b_elb_induction_budget) + (cf_head_elb_induction_budget)) * S ((cf_new_b_elb_induction_budget) + (cf_head_elb_induction_budget)) + ((cf_head_elb_induction_budget) + (cf_head_elb_induction_budget))) + (((cf_new_b_elb_induction_budget) + (cf_head_elb_induction_budget)) * S ((cf_new_b_elb_induction_budget) + (cf_head_elb_induction_budget)) + ((cf_head_elb_induction_budget) + (cf_head_elb_induction_budget))))) = S ((S (S cf_index_elb_induction_budget)) * elb_scale_induction)) /\ exists ff_q_cf_elb_induction_budget_following_state. elb_history_induction = ff_q_cf_elb_induction_budget_following_state * S ((S (S cf_index_elb_induction_budget)) * elb_scale_induction) + (((cf_new_a_elb_induction_budget) + (((cf_new_b_elb_induction_budget) + (cf_head_elb_induction_budget)) * S ((cf_new_b_elb_induction_budget) + (cf_head_elb_induction_budget)) + ((cf_head_elb_induction_budget) + (cf_head_elb_induction_budget)))) * S ((cf_new_a_elb_induction_budget) + (((cf_new_b_elb_induction_budget) + (cf_head_elb_induction_budget)) * S ((cf_new_b_elb_induction_budget) + (cf_head_elb_induction_budget)) + ((cf_head_elb_induction_budget) + (cf_head_elb_induction_budget)))) + ((((cf_new_b_elb_induction_budget) + (cf_head_elb_induction_budget)) * S ((cf_new_b_elb_induction_budget) + (cf_head_elb_induction_budget)) + ((cf_head_elb_induction_budget) + (cf_head_elb_induction_budget))) + (((cf_new_b_elb_induction_budget) + (cf_head_elb_induction_budget)) * S ((cf_new_b_elb_induction_budget) + (cf_head_elb_induction_budget)) + ((cf_head_elb_induction_budget) + (cf_head_elb_induction_budget))))))) /\ (cf_new_b_elb_induction_budget = cf_old_a_elb_induction_budget /\ (cf_new_a_elb_induction_budget = cf_new_b_elb_induction_budget * cf_quotient_elb_induction_budget + cf_old_b_elb_induction_budget /\ ((exists ff_lt_cf_elb_induction_budget_remainder. ff_lt_cf_elb_induction_budget_remainder + S cf_old_b_elb_induction_budget = cf_new_b_elb_induction_budget) /\ (cf_head_elb_induction_budget = S ((cf_quotient_elb_induction_budget + cf_tail_elb_induction_budget) * S (cf_quotient_elb_induction_budget + cf_tail_elb_induction_budget) + (cf_tail_elb_induction_budget + cf_tail_elb_induction_budget))))))))))) /\ exists elb_gap_induction. elb_gap_induction + elb_steps_induction = ((n + n))))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

135 script commands · 28 reading checkpoints · 14 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 (7)
euclidean log power zero divisoreuclidean log budget zero divisoreuclidean log budget extendeuclidean log budget weakeneuclidean log budget successor powereuclidean log halving power dropeuclidean log budget extend twice

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.

01Induction on nL1–6

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

  1. L1
    induction n
  2. L2
    intro p
  3. L3
    intro hpower
  4. L4
    intro b
  5. L5
    intro hbelow
  6. L6
    intro a
02Establish hzeroL7–16

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply euclidean log power zero divisor.

  1. L7
    have hzero : b = 0
  2. L8
    specialize euclidean_log_power_zero_divisor p
  3. L9
    specialize euclidean_log_power_zero_divisor b
  4. L10
    apply euclidean_log_power_zero_divisor
  5. L11
    exact hpower
  6. L12
    exact hbelow
  7. L13
    specialize euclidean_log_budget_zero_divisor a
  8. L14
    specialize euclidean_log_budget_zero_divisor b
  9. L15
    specialize euclidean_log_budget_zero_divisor (0 + 0)
  10. L16
    apply euclidean_log_budget_zero_divisor
03Use earlier factsL17–17

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

  1. L17
    exact hzero
04Fix variables and assumptionsL18–22

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

  1. L18
    intro p
  2. L19
    intro hpower
  3. L20
    intro b
  4. L21
    intro hbelow
  5. L22
    intro a
05Use earlier factsL23–23

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

  1. L23
    specialize binary_power_two_exists n
06Separate the logical casesL24–24

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

  1. L24
    cases binary_power_two_exists
07Establish hdoubleL25–33

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary power two successor double.

  1. L25
    have hdouble : p = x + x
  2. L26
    specialize binary_power_two_successor_double n
  3. L27
    specialize binary_power_two_successor_double x
  4. L28
    specialize binary_power_two_successor_double p
  5. L29
    apply binary_power_two_successor_double
  6. L30
    exact binary_power_two_exists_witness
  7. L31
    exact hpower
  8. L32
    specialize eq_decidable b
  9. L33
    specialize eq_decidable 0
08Separate the logical casesL34–34

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

  1. L34
    cases eq_decidable
09Use earlier factsL35–39

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

  1. L35
    specialize euclidean_log_budget_zero_divisor a
  2. L36
    specialize euclidean_log_budget_zero_divisor b
  3. L37
    specialize euclidean_log_budget_zero_divisor (S n + S n)
  4. L38
    apply euclidean_log_budget_zero_divisor
  5. L39
    exact eq_decidable_left
10Establish hfirstL40–44

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

  1. L40
    have hfirst : exists q r. ((a = b * q + r /\ (exists ff_lt_ec_elb_induction_first_division. ff_lt_ec_elb_induction_first_division + S r = b)))
  2. L41
    specialize euclidean_division_step_exists a
  3. L42
    specialize euclidean_division_step_exists b
  4. L43
    apply euclidean_division_step_exists
  5. L44
    exact eq_decidable_right
11Separate the logical casesL45–46

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

  1. L45
    cases hfirst
  2. L46
    cases hfirst_witness
12Use earlier factsL47–47

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

  1. L47
    specialize zero_or_succ x2
13Separate the logical casesL48–48

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

  1. L48
    cases zero_or_succ
14Establish hsmallL49–54

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply euclidean log budget zero divisor.

  1. L49
    have hsmall : EuclideanBoundedTrace(b,x2,n + n)Definitions: EuclideanBoundedTraceOriginal native command in the exact edition
  2. L50
    specialize euclidean_log_budget_zero_divisor b
  3. L51
    specialize euclidean_log_budget_zero_divisor x2
  4. L52
    specialize euclidean_log_budget_zero_divisor (n + n)
  5. L53
    apply euclidean_log_budget_zero_divisor
  6. L54
    exact zero_or_succ_left
15Establish hfirst_budgetL55–63

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply euclidean log budget extend.

  1. L55
    have hfirst_budget : EuclideanBoundedTrace(a,b,S (n + n))Definitions: EuclideanBoundedTraceOriginal native command in the exact edition
  2. L56
    specialize euclidean_log_budget_extend a
  3. L57
    specialize euclidean_log_budget_extend b
  4. L58
    specialize euclidean_log_budget_extend x1
  5. L59
    specialize euclidean_log_budget_extend x2
  6. L60
    specialize euclidean_log_budget_extend (n + n)
  7. L61
    apply euclidean_log_budget_extend
  8. L62
    exact hfirst_witness_witness
  9. L63
    exact hsmall
16Establish hweakenedL64–73

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply euclidean log budget weaken.

  1. L64
    have hweakened : EuclideanBoundedTrace(a,b,S S (n + n))Definitions: EuclideanBoundedTraceOriginal native command in the exact edition
  2. L65
    specialize euclidean_log_budget_weaken a
  3. L66
    specialize euclidean_log_budget_weaken b
  4. L67
    specialize euclidean_log_budget_weaken (S (n + n))
  5. L68
    apply euclidean_log_budget_weaken
  6. L69
    exact hfirst_budget
  7. L70
    specialize euclidean_log_budget_successor_power a
  8. L71
    specialize euclidean_log_budget_successor_power b
  9. L72
    specialize euclidean_log_budget_successor_power n
  10. L73
    apply euclidean_log_budget_successor_power
17Use earlier factsL74–74

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

  1. L74
    exact hweakened
18Separate the logical casesL75–75

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

  1. L75
    cases zero_or_succ_right
19Establish hnonzeroL76–84

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

  1. L76
    have hnonzero : ~(x2 = 0)
  2. L77
    intro hzero
  3. L78
    apply PA1
  4. L79
    trans x2
  5. L80
    symm
  6. L81
    exact zero_or_succ_right_witness
  7. L82
    exact hzero
  8. L83
    specialize division_remainder_exists x2
  9. L84
    specialize division_remainder_exists b
20Establish hsecondL85–87

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

  1. L85
    have hsecond : exists Q t. ((b = x2 * Q + t /\ (exists ff_lt_ec_elb_induction_second_division. ff_lt_ec_elb_induction_second_division + S t = x2)))
  2. L86
    apply division_remainder_exists
  3. L87
    exact hnonzero
21Separate the logical casesL88–89

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

  1. L88
    cases hsecond
  2. L89
    cases hsecond_witness
22Establish hhalfL90–99

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply euclidean two step halving.

  1. L90
    have hhalf : exists gap. gap + S (x5 + x5) = b
  2. L91
    specialize euclidean_two_step_halving a
  3. L92
    specialize euclidean_two_step_halving b
  4. L93
    specialize euclidean_two_step_halving x1
  5. L94
    specialize euclidean_two_step_halving x2
  6. L95
    specialize euclidean_two_step_halving x4
  7. L96
    specialize euclidean_two_step_halving x5
  8. L97
    apply euclidean_two_step_halving
  9. L98
    exact hfirst_witness_witness
  10. L99
    exact hsecond_witness_witness
23Establish hupperL100–102

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

  1. L100
    have hupper : exists gap. gap + S b = x + x
  2. L101
    rewrite hdouble at hbelow
  3. L102
    exact hbelow
24Establish hdropL103–110

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply euclidean log halving power drop.

  1. L103
    have hdrop : exists gap. gap + S x5 = x
  2. L104
    specialize euclidean_log_halving_power_drop b
  3. L105
    specialize euclidean_log_halving_power_drop x5
  4. L106
    specialize euclidean_log_halving_power_drop x
  5. L107
    apply euclidean_log_halving_power_drop
  6. L108
    exact hhalf
  7. L109
    exact hupper
  8. L110
    specialize IH x
25Establish hboundedL111–114

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

  1. L111
    have hbounded : ∀ b. Lt(b,x) → ∀ y. EuclideanBoundedTrace(y,b,n + n)Definitions: EuclideanBoundedTraceLtOriginal native command in the exact edition
  2. L112
    apply IH
  3. L113
    exact binary_power_two_exists_witness
  4. L114
    specialize hbounded x5
26Establish hallL115–118

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

  1. L115
    have hall : ∀ z. EuclideanBoundedTrace(z,x5,n + n)Definitions: EuclideanBoundedTraceOriginal native command in the exact edition
  2. L116
    apply hbounded
  3. L117
    exact hdrop
  4. L118
    specialize hall x2
27Establish htwiceL119–128

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply euclidean log budget extend twice.

  1. L119
    have htwice : EuclideanBoundedTrace(a,b,S S (n + n))Definitions: EuclideanBoundedTraceOriginal native command in the exact edition
  2. L120
    specialize euclidean_log_budget_extend_twice a
  3. L121
    specialize euclidean_log_budget_extend_twice b
  4. L122
    specialize euclidean_log_budget_extend_twice x1
  5. L123
    specialize euclidean_log_budget_extend_twice x2
  6. L124
    specialize euclidean_log_budget_extend_twice x4
  7. L125
    specialize euclidean_log_budget_extend_twice x5
  8. L126
    specialize euclidean_log_budget_extend_twice (n + n)
  9. L127
    apply euclidean_log_budget_extend_twice
  10. L128
    exact hfirst_witness_witness
28Use earlier factsL129–135

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

  1. L129
    exact hsecond_witness_witness
  2. L130
    exact hall
  3. L131
    specialize euclidean_log_budget_successor_power a
  4. L132
    specialize euclidean_log_budget_successor_power b
  5. L133
    specialize euclidean_log_budget_successor_power n
  6. L134
    apply euclidean_log_budget_successor_power
  7. L135
    exact htwice

Library-wide reading audit

Original defined command ledger · 135 lines
  1. 0001induction n
  2. 0002intro p
  3. 0003intro hpower
  4. 0004intro b
  5. 0005intro hbelow
  6. 0006intro a
  7. 0007have hzero : b = 0
  8. 0008specialize euclidean_log_power_zero_divisor p
  9. 0009specialize euclidean_log_power_zero_divisor b
  10. 0010apply euclidean_log_power_zero_divisor
  11. 0011exact hpower
  12. 0012exact hbelow
  13. 0013specialize euclidean_log_budget_zero_divisor a
  14. 0014specialize euclidean_log_budget_zero_divisor b
  15. 0015specialize euclidean_log_budget_zero_divisor (0 + 0)
  16. 0016apply euclidean_log_budget_zero_divisor
  17. 0017exact hzero
  18. 0018intro p
  19. 0019intro hpower
  20. 0020intro b
  21. 0021intro hbelow
  22. 0022intro a
  23. 0023specialize binary_power_two_exists n
  24. 0024cases binary_power_two_exists
  25. 0025have hdouble : p = x + x
  26. 0026specialize binary_power_two_successor_double n
  27. 0027specialize binary_power_two_successor_double x
  28. 0028specialize binary_power_two_successor_double p
  29. 0029apply binary_power_two_successor_double
  30. 0030exact binary_power_two_exists_witness
  31. 0031exact hpower
  32. 0032specialize eq_decidable b
  33. 0033specialize eq_decidable 0
  34. 0034cases eq_decidable
  35. 0035specialize euclidean_log_budget_zero_divisor a
  36. 0036specialize euclidean_log_budget_zero_divisor b
  37. 0037specialize euclidean_log_budget_zero_divisor (S n + S n)
  38. 0038apply euclidean_log_budget_zero_divisor
  39. 0039exact eq_decidable_left
  40. 0040have hfirst : exists q r. ((a = b * q + r /\ (exists ff_lt_ec_elb_induction_first_division. ff_lt_ec_elb_induction_first_division + S r = b)))
  41. 0041specialize euclidean_division_step_exists a
  42. 0042specialize euclidean_division_step_exists b
  43. 0043apply euclidean_division_step_exists
  44. 0044exact eq_decidable_right
  45. 0045cases hfirst
  46. 0046cases hfirst_witness
  47. 0047specialize zero_or_succ x2
  48. 0048cases zero_or_succ
  49. 0049have hsmall : exists elb_list_zero_remainder elb_history_zero_remainder elb_scale_zero_remainder elb_steps_zero_remainder. ((exists cf_gcd_elb_zero_remainder_budget. ((((exists ff_h_cf_elb_zero_remainder_budget_initial_state. ff_h_cf_elb_zero_remainder_budget_initial_state + S (((cf_gcd_elb_zero_remainder_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_zero_remainder_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * elb_scale_zero_remainder)) /\ exists ff_q_cf_elb_zero_remainder_budget_initial_state. elb_history_zero_remainder = ff_q_cf_elb_zero_remainder_budget_initial_state * S ((S (0)) * elb_scale_zero_remainder) + (((cf_gcd_elb_zero_remainder_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_zero_remainder_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))))) /\ ((((exists ff_h_cf_elb_zero_remainder_budget_terminal_state. ff_h_cf_elb_zero_remainder_budget_terminal_state + S (((b) + (((x2) + (elb_list_zero_remainder)) * S ((x2) + (elb_list_zero_remainder)) + ((elb_list_zero_remainder) + (elb_list_zero_remainder)))) * S ((b) + (((x2) + (elb_list_zero_remainder)) * S ((x2) + (elb_list_zero_remainder)) + ((elb_list_zero_remainder) + (elb_list_zero_remainder)))) + ((((x2) + (elb_list_zero_remainder)) * S ((x2) + (elb_list_zero_remainder)) + ((elb_list_zero_remainder) + (elb_list_zero_remainder))) + (((x2) + (elb_list_zero_remainder)) * S ((x2) + (elb_list_zero_remainder)) + ((elb_list_zero_remainder) + (elb_list_zero_remainder))))) = S ((S (elb_steps_zero_remainder)) * elb_scale_zero_remainder)) /\ exists ff_q_cf_elb_zero_remainder_budget_terminal_state. elb_history_zero_remainder = ff_q_cf_elb_zero_remainder_budget_terminal_state * S ((S (elb_steps_zero_remainder)) * elb_scale_zero_remainder) + (((b) + (((x2) + (elb_list_zero_remainder)) * S ((x2) + (elb_list_zero_remainder)) + ((elb_list_zero_remainder) + (elb_list_zero_remainder)))) * S ((b) + (((x2) + (elb_list_zero_remainder)) * S ((x2) + (elb_list_zero_remainder)) + ((elb_list_zero_remainder) + (elb_list_zero_remainder)))) + ((((x2) + (elb_list_zero_remainder)) * S ((x2) + (elb_list_zero_remainder)) + ((elb_list_zero_remainder) + (elb_list_zero_remainder))) + (((x2) + (elb_list_zero_remainder)) * S ((x2) + (elb_list_zero_remainder)) + ((elb_list_zero_remainder) + (elb_list_zero_remainder))))))) /\ forall cf_index_elb_zero_remainder_budget. (exists ff_lt_cf_elb_zero_remainder_budget_index. ff_lt_cf_elb_zero_remainder_budget_index + S cf_index_elb_zero_remainder_budget = elb_steps_zero_remainder) -> exists cf_old_a_elb_zero_remainder_budget cf_old_b_elb_zero_remainder_budget cf_tail_elb_zero_remainder_budget cf_new_a_elb_zero_remainder_budget cf_new_b_elb_zero_remainder_budget cf_head_elb_zero_remainder_budget cf_quotient_elb_zero_remainder_budget. ((((exists ff_h_cf_elb_zero_remainder_budget_previous_state. ff_h_cf_elb_zero_remainder_budget_previous_state + S (((cf_old_a_elb_zero_remainder_budget) + (((cf_old_b_elb_zero_remainder_budget) + (cf_tail_elb_zero_remainder_budget)) * S ((cf_old_b_elb_zero_remainder_budget) + (cf_tail_elb_zero_remainder_budget)) + ((cf_tail_elb_zero_remainder_budget) + (cf_tail_elb_zero_remainder_budget)))) * S ((cf_old_a_elb_zero_remainder_budget) + (((cf_old_b_elb_zero_remainder_budget) + (cf_tail_elb_zero_remainder_budget)) * S ((cf_old_b_elb_zero_remainder_budget) + (cf_tail_elb_zero_remainder_budget)) + ((cf_tail_elb_zero_remainder_budget) + (cf_tail_elb_zero_remainder_budget)))) + ((((cf_old_b_elb_zero_remainder_budget) + (cf_tail_elb_zero_remainder_budget)) * S ((cf_old_b_elb_zero_remainder_budget) + (cf_tail_elb_zero_remainder_budget)) + ((cf_tail_elb_zero_remainder_budget) + (cf_tail_elb_zero_remainder_budget))) + (((cf_old_b_elb_zero_remainder_budget) + (cf_tail_elb_zero_remainder_budget)) * S ((cf_old_b_elb_zero_remainder_budget) + (cf_tail_elb_zero_remainder_budget)) + ((cf_tail_elb_zero_remainder_budget) + (cf_tail_elb_zero_remainder_budget))))) = S ((S (cf_index_elb_zero_remainder_budget)) * elb_scale_zero_remainder)) /\ exists ff_q_cf_elb_zero_remainder_budget_previous_state. elb_history_zero_remainder = ff_q_cf_elb_zero_remainder_budget_previous_state * S ((S (cf_index_elb_zero_remainder_budget)) * elb_scale_zero_remainder) + (((cf_old_a_elb_zero_remainder_budget) + (((cf_old_b_elb_zero_remainder_budget) + (cf_tail_elb_zero_remainder_budget)) * S ((cf_old_b_elb_zero_remainder_budget) + (cf_tail_elb_zero_remainder_budget)) + ((cf_tail_elb_zero_remainder_budget) + (cf_tail_elb_zero_remainder_budget)))) * S ((cf_old_a_elb_zero_remainder_budget) + (((cf_old_b_elb_zero_remainder_budget) + (cf_tail_elb_zero_remainder_budget)) * S ((cf_old_b_elb_zero_remainder_budget) + (cf_tail_elb_zero_remainder_budget)) + ((cf_tail_elb_zero_remainder_budget) + (cf_tail_elb_zero_remainder_budget)))) + ((((cf_old_b_elb_zero_remainder_budget) + (cf_tail_elb_zero_remainder_budget)) * S ((cf_old_b_elb_zero_remainder_budget) + (cf_tail_elb_zero_remainder_budget)) + ((cf_tail_elb_zero_remainder_budget) + (cf_tail_elb_zero_remainder_budget))) + (((cf_old_b_elb_zero_remainder_budget) + (cf_tail_elb_zero_remainder_budget)) * S ((cf_old_b_elb_zero_remainder_budget) + (cf_tail_elb_zero_remainder_budget)) + ((cf_tail_elb_zero_remainder_budget) + (cf_tail_elb_zero_remainder_budget))))))) /\ ((((exists ff_h_cf_elb_zero_remainder_budget_following_state. ff_h_cf_elb_zero_remainder_budget_following_state + S (((cf_new_a_elb_zero_remainder_budget) + (((cf_new_b_elb_zero_remainder_budget) + (cf_head_elb_zero_remainder_budget)) * S ((cf_new_b_elb_zero_remainder_budget) + (cf_head_elb_zero_remainder_budget)) + ((cf_head_elb_zero_remainder_budget) + (cf_head_elb_zero_remainder_budget)))) * S ((cf_new_a_elb_zero_remainder_budget) + (((cf_new_b_elb_zero_remainder_budget) + (cf_head_elb_zero_remainder_budget)) * S ((cf_new_b_elb_zero_remainder_budget) + (cf_head_elb_zero_remainder_budget)) + ((cf_head_elb_zero_remainder_budget) + (cf_head_elb_zero_remainder_budget)))) + ((((cf_new_b_elb_zero_remainder_budget) + (cf_head_elb_zero_remainder_budget)) * S ((cf_new_b_elb_zero_remainder_budget) + (cf_head_elb_zero_remainder_budget)) + ((cf_head_elb_zero_remainder_budget) + (cf_head_elb_zero_remainder_budget))) + (((cf_new_b_elb_zero_remainder_budget) + (cf_head_elb_zero_remainder_budget)) * S ((cf_new_b_elb_zero_remainder_budget) + (cf_head_elb_zero_remainder_budget)) + ((cf_head_elb_zero_remainder_budget) + (cf_head_elb_zero_remainder_budget))))) = S ((S (S cf_index_elb_zero_remainder_budget)) * elb_scale_zero_remainder)) /\ exists ff_q_cf_elb_zero_remainder_budget_following_state. elb_history_zero_remainder = ff_q_cf_elb_zero_remainder_budget_following_state * S ((S (S cf_index_elb_zero_remainder_budget)) * elb_scale_zero_remainder) + (((cf_new_a_elb_zero_remainder_budget) + (((cf_new_b_elb_zero_remainder_budget) + (cf_head_elb_zero_remainder_budget)) * S ((cf_new_b_elb_zero_remainder_budget) + (cf_head_elb_zero_remainder_budget)) + ((cf_head_elb_zero_remainder_budget) + (cf_head_elb_zero_remainder_budget)))) * S ((cf_new_a_elb_zero_remainder_budget) + (((cf_new_b_elb_zero_remainder_budget) + (cf_head_elb_zero_remainder_budget)) * S ((cf_new_b_elb_zero_remainder_budget) + (cf_head_elb_zero_remainder_budget)) + ((cf_head_elb_zero_remainder_budget) + (cf_head_elb_zero_remainder_budget)))) + ((((cf_new_b_elb_zero_remainder_budget) + (cf_head_elb_zero_remainder_budget)) * S ((cf_new_b_elb_zero_remainder_budget) + (cf_head_elb_zero_remainder_budget)) + ((cf_head_elb_zero_remainder_budget) + (cf_head_elb_zero_remainder_budget))) + (((cf_new_b_elb_zero_remainder_budget) + (cf_head_elb_zero_remainder_budget)) * S ((cf_new_b_elb_zero_remainder_budget) + (cf_head_elb_zero_remainder_budget)) + ((cf_head_elb_zero_remainder_budget) + (cf_head_elb_zero_remainder_budget))))))) /\ (cf_new_b_elb_zero_remainder_budget = cf_old_a_elb_zero_remainder_budget /\ (cf_new_a_elb_zero_remainder_budget = cf_new_b_elb_zero_remainder_budget * cf_quotient_elb_zero_remainder_budget + cf_old_b_elb_zero_remainder_budget /\ ((exists ff_lt_cf_elb_zero_remainder_budget_remainder. ff_lt_cf_elb_zero_remainder_budget_remainder + S cf_old_b_elb_zero_remainder_budget = cf_new_b_elb_zero_remainder_budget) /\ (cf_head_elb_zero_remainder_budget = S ((cf_quotient_elb_zero_remainder_budget + cf_tail_elb_zero_remainder_budget) * S (cf_quotient_elb_zero_remainder_budget + cf_tail_elb_zero_remainder_budget) + (cf_tail_elb_zero_remainder_budget + cf_tail_elb_zero_remainder_budget))))))))))) /\ exists elb_gap_zero_remainder. elb_gap_zero_remainder + elb_steps_zero_remainder = ((n + n)))
  50. 0050specialize euclidean_log_budget_zero_divisor b
  51. 0051specialize euclidean_log_budget_zero_divisor x2
  52. 0052specialize euclidean_log_budget_zero_divisor (n + n)
  53. 0053apply euclidean_log_budget_zero_divisor
  54. 0054exact zero_or_succ_left
  55. 0055have hfirst_budget : exists elb_list_first_budget elb_history_first_budget elb_scale_first_budget elb_steps_first_budget. ((exists cf_gcd_elb_first_budget_budget. ((((exists ff_h_cf_elb_first_budget_budget_initial_state. ff_h_cf_elb_first_budget_budget_initial_state + S (((cf_gcd_elb_first_budget_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_first_budget_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * elb_scale_first_budget)) /\ exists ff_q_cf_elb_first_budget_budget_initial_state. elb_history_first_budget = ff_q_cf_elb_first_budget_budget_initial_state * S ((S (0)) * elb_scale_first_budget) + (((cf_gcd_elb_first_budget_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_first_budget_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))))) /\ ((((exists ff_h_cf_elb_first_budget_budget_terminal_state. ff_h_cf_elb_first_budget_budget_terminal_state + S (((a) + (((b) + (elb_list_first_budget)) * S ((b) + (elb_list_first_budget)) + ((elb_list_first_budget) + (elb_list_first_budget)))) * S ((a) + (((b) + (elb_list_first_budget)) * S ((b) + (elb_list_first_budget)) + ((elb_list_first_budget) + (elb_list_first_budget)))) + ((((b) + (elb_list_first_budget)) * S ((b) + (elb_list_first_budget)) + ((elb_list_first_budget) + (elb_list_first_budget))) + (((b) + (elb_list_first_budget)) * S ((b) + (elb_list_first_budget)) + ((elb_list_first_budget) + (elb_list_first_budget))))) = S ((S (elb_steps_first_budget)) * elb_scale_first_budget)) /\ exists ff_q_cf_elb_first_budget_budget_terminal_state. elb_history_first_budget = ff_q_cf_elb_first_budget_budget_terminal_state * S ((S (elb_steps_first_budget)) * elb_scale_first_budget) + (((a) + (((b) + (elb_list_first_budget)) * S ((b) + (elb_list_first_budget)) + ((elb_list_first_budget) + (elb_list_first_budget)))) * S ((a) + (((b) + (elb_list_first_budget)) * S ((b) + (elb_list_first_budget)) + ((elb_list_first_budget) + (elb_list_first_budget)))) + ((((b) + (elb_list_first_budget)) * S ((b) + (elb_list_first_budget)) + ((elb_list_first_budget) + (elb_list_first_budget))) + (((b) + (elb_list_first_budget)) * S ((b) + (elb_list_first_budget)) + ((elb_list_first_budget) + (elb_list_first_budget))))))) /\ forall cf_index_elb_first_budget_budget. (exists ff_lt_cf_elb_first_budget_budget_index. ff_lt_cf_elb_first_budget_budget_index + S cf_index_elb_first_budget_budget = elb_steps_first_budget) -> exists cf_old_a_elb_first_budget_budget cf_old_b_elb_first_budget_budget cf_tail_elb_first_budget_budget cf_new_a_elb_first_budget_budget cf_new_b_elb_first_budget_budget cf_head_elb_first_budget_budget cf_quotient_elb_first_budget_budget. ((((exists ff_h_cf_elb_first_budget_budget_previous_state. ff_h_cf_elb_first_budget_budget_previous_state + S (((cf_old_a_elb_first_budget_budget) + (((cf_old_b_elb_first_budget_budget) + (cf_tail_elb_first_budget_budget)) * S ((cf_old_b_elb_first_budget_budget) + (cf_tail_elb_first_budget_budget)) + ((cf_tail_elb_first_budget_budget) + (cf_tail_elb_first_budget_budget)))) * S ((cf_old_a_elb_first_budget_budget) + (((cf_old_b_elb_first_budget_budget) + (cf_tail_elb_first_budget_budget)) * S ((cf_old_b_elb_first_budget_budget) + (cf_tail_elb_first_budget_budget)) + ((cf_tail_elb_first_budget_budget) + (cf_tail_elb_first_budget_budget)))) + ((((cf_old_b_elb_first_budget_budget) + (cf_tail_elb_first_budget_budget)) * S ((cf_old_b_elb_first_budget_budget) + (cf_tail_elb_first_budget_budget)) + ((cf_tail_elb_first_budget_budget) + (cf_tail_elb_first_budget_budget))) + (((cf_old_b_elb_first_budget_budget) + (cf_tail_elb_first_budget_budget)) * S ((cf_old_b_elb_first_budget_budget) + (cf_tail_elb_first_budget_budget)) + ((cf_tail_elb_first_budget_budget) + (cf_tail_elb_first_budget_budget))))) = S ((S (cf_index_elb_first_budget_budget)) * elb_scale_first_budget)) /\ exists ff_q_cf_elb_first_budget_budget_previous_state. elb_history_first_budget = ff_q_cf_elb_first_budget_budget_previous_state * S ((S (cf_index_elb_first_budget_budget)) * elb_scale_first_budget) + (((cf_old_a_elb_first_budget_budget) + (((cf_old_b_elb_first_budget_budget) + (cf_tail_elb_first_budget_budget)) * S ((cf_old_b_elb_first_budget_budget) + (cf_tail_elb_first_budget_budget)) + ((cf_tail_elb_first_budget_budget) + (cf_tail_elb_first_budget_budget)))) * S ((cf_old_a_elb_first_budget_budget) + (((cf_old_b_elb_first_budget_budget) + (cf_tail_elb_first_budget_budget)) * S ((cf_old_b_elb_first_budget_budget) + (cf_tail_elb_first_budget_budget)) + ((cf_tail_elb_first_budget_budget) + (cf_tail_elb_first_budget_budget)))) + ((((cf_old_b_elb_first_budget_budget) + (cf_tail_elb_first_budget_budget)) * S ((cf_old_b_elb_first_budget_budget) + (cf_tail_elb_first_budget_budget)) + ((cf_tail_elb_first_budget_budget) + (cf_tail_elb_first_budget_budget))) + (((cf_old_b_elb_first_budget_budget) + (cf_tail_elb_first_budget_budget)) * S ((cf_old_b_elb_first_budget_budget) + (cf_tail_elb_first_budget_budget)) + ((cf_tail_elb_first_budget_budget) + (cf_tail_elb_first_budget_budget))))))) /\ ((((exists ff_h_cf_elb_first_budget_budget_following_state. ff_h_cf_elb_first_budget_budget_following_state + S (((cf_new_a_elb_first_budget_budget) + (((cf_new_b_elb_first_budget_budget) + (cf_head_elb_first_budget_budget)) * S ((cf_new_b_elb_first_budget_budget) + (cf_head_elb_first_budget_budget)) + ((cf_head_elb_first_budget_budget) + (cf_head_elb_first_budget_budget)))) * S ((cf_new_a_elb_first_budget_budget) + (((cf_new_b_elb_first_budget_budget) + (cf_head_elb_first_budget_budget)) * S ((cf_new_b_elb_first_budget_budget) + (cf_head_elb_first_budget_budget)) + ((cf_head_elb_first_budget_budget) + (cf_head_elb_first_budget_budget)))) + ((((cf_new_b_elb_first_budget_budget) + (cf_head_elb_first_budget_budget)) * S ((cf_new_b_elb_first_budget_budget) + (cf_head_elb_first_budget_budget)) + ((cf_head_elb_first_budget_budget) + (cf_head_elb_first_budget_budget))) + (((cf_new_b_elb_first_budget_budget) + (cf_head_elb_first_budget_budget)) * S ((cf_new_b_elb_first_budget_budget) + (cf_head_elb_first_budget_budget)) + ((cf_head_elb_first_budget_budget) + (cf_head_elb_first_budget_budget))))) = S ((S (S cf_index_elb_first_budget_budget)) * elb_scale_first_budget)) /\ exists ff_q_cf_elb_first_budget_budget_following_state. elb_history_first_budget = ff_q_cf_elb_first_budget_budget_following_state * S ((S (S cf_index_elb_first_budget_budget)) * elb_scale_first_budget) + (((cf_new_a_elb_first_budget_budget) + (((cf_new_b_elb_first_budget_budget) + (cf_head_elb_first_budget_budget)) * S ((cf_new_b_elb_first_budget_budget) + (cf_head_elb_first_budget_budget)) + ((cf_head_elb_first_budget_budget) + (cf_head_elb_first_budget_budget)))) * S ((cf_new_a_elb_first_budget_budget) + (((cf_new_b_elb_first_budget_budget) + (cf_head_elb_first_budget_budget)) * S ((cf_new_b_elb_first_budget_budget) + (cf_head_elb_first_budget_budget)) + ((cf_head_elb_first_budget_budget) + (cf_head_elb_first_budget_budget)))) + ((((cf_new_b_elb_first_budget_budget) + (cf_head_elb_first_budget_budget)) * S ((cf_new_b_elb_first_budget_budget) + (cf_head_elb_first_budget_budget)) + ((cf_head_elb_first_budget_budget) + (cf_head_elb_first_budget_budget))) + (((cf_new_b_elb_first_budget_budget) + (cf_head_elb_first_budget_budget)) * S ((cf_new_b_elb_first_budget_budget) + (cf_head_elb_first_budget_budget)) + ((cf_head_elb_first_budget_budget) + (cf_head_elb_first_budget_budget))))))) /\ (cf_new_b_elb_first_budget_budget = cf_old_a_elb_first_budget_budget /\ (cf_new_a_elb_first_budget_budget = cf_new_b_elb_first_budget_budget * cf_quotient_elb_first_budget_budget + cf_old_b_elb_first_budget_budget /\ ((exists ff_lt_cf_elb_first_budget_budget_remainder. ff_lt_cf_elb_first_budget_budget_remainder + S cf_old_b_elb_first_budget_budget = cf_new_b_elb_first_budget_budget) /\ (cf_head_elb_first_budget_budget = S ((cf_quotient_elb_first_budget_budget + cf_tail_elb_first_budget_budget) * S (cf_quotient_elb_first_budget_budget + cf_tail_elb_first_budget_budget) + (cf_tail_elb_first_budget_budget + cf_tail_elb_first_budget_budget))))))))))) /\ exists elb_gap_first_budget. elb_gap_first_budget + elb_steps_first_budget = (S (n + n)))
  56. 0056specialize euclidean_log_budget_extend a
  57. 0057specialize euclidean_log_budget_extend b
  58. 0058specialize euclidean_log_budget_extend x1
  59. 0059specialize euclidean_log_budget_extend x2
  60. 0060specialize euclidean_log_budget_extend (n + n)
  61. 0061apply euclidean_log_budget_extend
  62. 0062exact hfirst_witness_witness
  63. 0063exact hsmall
  64. 0064have hweakened : exists elb_list_one_weakened elb_history_one_weakened elb_scale_one_weakened elb_steps_one_weakened. ((exists cf_gcd_elb_one_weakened_budget. ((((exists ff_h_cf_elb_one_weakened_budget_initial_state. ff_h_cf_elb_one_weakened_budget_initial_state + S (((cf_gcd_elb_one_weakened_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_one_weakened_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * elb_scale_one_weakened)) /\ exists ff_q_cf_elb_one_weakened_budget_initial_state. elb_history_one_weakened = ff_q_cf_elb_one_weakened_budget_initial_state * S ((S (0)) * elb_scale_one_weakened) + (((cf_gcd_elb_one_weakened_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_one_weakened_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))))) /\ ((((exists ff_h_cf_elb_one_weakened_budget_terminal_state. ff_h_cf_elb_one_weakened_budget_terminal_state + S (((a) + (((b) + (elb_list_one_weakened)) * S ((b) + (elb_list_one_weakened)) + ((elb_list_one_weakened) + (elb_list_one_weakened)))) * S ((a) + (((b) + (elb_list_one_weakened)) * S ((b) + (elb_list_one_weakened)) + ((elb_list_one_weakened) + (elb_list_one_weakened)))) + ((((b) + (elb_list_one_weakened)) * S ((b) + (elb_list_one_weakened)) + ((elb_list_one_weakened) + (elb_list_one_weakened))) + (((b) + (elb_list_one_weakened)) * S ((b) + (elb_list_one_weakened)) + ((elb_list_one_weakened) + (elb_list_one_weakened))))) = S ((S (elb_steps_one_weakened)) * elb_scale_one_weakened)) /\ exists ff_q_cf_elb_one_weakened_budget_terminal_state. elb_history_one_weakened = ff_q_cf_elb_one_weakened_budget_terminal_state * S ((S (elb_steps_one_weakened)) * elb_scale_one_weakened) + (((a) + (((b) + (elb_list_one_weakened)) * S ((b) + (elb_list_one_weakened)) + ((elb_list_one_weakened) + (elb_list_one_weakened)))) * S ((a) + (((b) + (elb_list_one_weakened)) * S ((b) + (elb_list_one_weakened)) + ((elb_list_one_weakened) + (elb_list_one_weakened)))) + ((((b) + (elb_list_one_weakened)) * S ((b) + (elb_list_one_weakened)) + ((elb_list_one_weakened) + (elb_list_one_weakened))) + (((b) + (elb_list_one_weakened)) * S ((b) + (elb_list_one_weakened)) + ((elb_list_one_weakened) + (elb_list_one_weakened))))))) /\ forall cf_index_elb_one_weakened_budget. (exists ff_lt_cf_elb_one_weakened_budget_index. ff_lt_cf_elb_one_weakened_budget_index + S cf_index_elb_one_weakened_budget = elb_steps_one_weakened) -> exists cf_old_a_elb_one_weakened_budget cf_old_b_elb_one_weakened_budget cf_tail_elb_one_weakened_budget cf_new_a_elb_one_weakened_budget cf_new_b_elb_one_weakened_budget cf_head_elb_one_weakened_budget cf_quotient_elb_one_weakened_budget. ((((exists ff_h_cf_elb_one_weakened_budget_previous_state. ff_h_cf_elb_one_weakened_budget_previous_state + S (((cf_old_a_elb_one_weakened_budget) + (((cf_old_b_elb_one_weakened_budget) + (cf_tail_elb_one_weakened_budget)) * S ((cf_old_b_elb_one_weakened_budget) + (cf_tail_elb_one_weakened_budget)) + ((cf_tail_elb_one_weakened_budget) + (cf_tail_elb_one_weakened_budget)))) * S ((cf_old_a_elb_one_weakened_budget) + (((cf_old_b_elb_one_weakened_budget) + (cf_tail_elb_one_weakened_budget)) * S ((cf_old_b_elb_one_weakened_budget) + (cf_tail_elb_one_weakened_budget)) + ((cf_tail_elb_one_weakened_budget) + (cf_tail_elb_one_weakened_budget)))) + ((((cf_old_b_elb_one_weakened_budget) + (cf_tail_elb_one_weakened_budget)) * S ((cf_old_b_elb_one_weakened_budget) + (cf_tail_elb_one_weakened_budget)) + ((cf_tail_elb_one_weakened_budget) + (cf_tail_elb_one_weakened_budget))) + (((cf_old_b_elb_one_weakened_budget) + (cf_tail_elb_one_weakened_budget)) * S ((cf_old_b_elb_one_weakened_budget) + (cf_tail_elb_one_weakened_budget)) + ((cf_tail_elb_one_weakened_budget) + (cf_tail_elb_one_weakened_budget))))) = S ((S (cf_index_elb_one_weakened_budget)) * elb_scale_one_weakened)) /\ exists ff_q_cf_elb_one_weakened_budget_previous_state. elb_history_one_weakened = ff_q_cf_elb_one_weakened_budget_previous_state * S ((S (cf_index_elb_one_weakened_budget)) * elb_scale_one_weakened) + (((cf_old_a_elb_one_weakened_budget) + (((cf_old_b_elb_one_weakened_budget) + (cf_tail_elb_one_weakened_budget)) * S ((cf_old_b_elb_one_weakened_budget) + (cf_tail_elb_one_weakened_budget)) + ((cf_tail_elb_one_weakened_budget) + (cf_tail_elb_one_weakened_budget)))) * S ((cf_old_a_elb_one_weakened_budget) + (((cf_old_b_elb_one_weakened_budget) + (cf_tail_elb_one_weakened_budget)) * S ((cf_old_b_elb_one_weakened_budget) + (cf_tail_elb_one_weakened_budget)) + ((cf_tail_elb_one_weakened_budget) + (cf_tail_elb_one_weakened_budget)))) + ((((cf_old_b_elb_one_weakened_budget) + (cf_tail_elb_one_weakened_budget)) * S ((cf_old_b_elb_one_weakened_budget) + (cf_tail_elb_one_weakened_budget)) + ((cf_tail_elb_one_weakened_budget) + (cf_tail_elb_one_weakened_budget))) + (((cf_old_b_elb_one_weakened_budget) + (cf_tail_elb_one_weakened_budget)) * S ((cf_old_b_elb_one_weakened_budget) + (cf_tail_elb_one_weakened_budget)) + ((cf_tail_elb_one_weakened_budget) + (cf_tail_elb_one_weakened_budget))))))) /\ ((((exists ff_h_cf_elb_one_weakened_budget_following_state. ff_h_cf_elb_one_weakened_budget_following_state + S (((cf_new_a_elb_one_weakened_budget) + (((cf_new_b_elb_one_weakened_budget) + (cf_head_elb_one_weakened_budget)) * S ((cf_new_b_elb_one_weakened_budget) + (cf_head_elb_one_weakened_budget)) + ((cf_head_elb_one_weakened_budget) + (cf_head_elb_one_weakened_budget)))) * S ((cf_new_a_elb_one_weakened_budget) + (((cf_new_b_elb_one_weakened_budget) + (cf_head_elb_one_weakened_budget)) * S ((cf_new_b_elb_one_weakened_budget) + (cf_head_elb_one_weakened_budget)) + ((cf_head_elb_one_weakened_budget) + (cf_head_elb_one_weakened_budget)))) + ((((cf_new_b_elb_one_weakened_budget) + (cf_head_elb_one_weakened_budget)) * S ((cf_new_b_elb_one_weakened_budget) + (cf_head_elb_one_weakened_budget)) + ((cf_head_elb_one_weakened_budget) + (cf_head_elb_one_weakened_budget))) + (((cf_new_b_elb_one_weakened_budget) + (cf_head_elb_one_weakened_budget)) * S ((cf_new_b_elb_one_weakened_budget) + (cf_head_elb_one_weakened_budget)) + ((cf_head_elb_one_weakened_budget) + (cf_head_elb_one_weakened_budget))))) = S ((S (S cf_index_elb_one_weakened_budget)) * elb_scale_one_weakened)) /\ exists ff_q_cf_elb_one_weakened_budget_following_state. elb_history_one_weakened = ff_q_cf_elb_one_weakened_budget_following_state * S ((S (S cf_index_elb_one_weakened_budget)) * elb_scale_one_weakened) + (((cf_new_a_elb_one_weakened_budget) + (((cf_new_b_elb_one_weakened_budget) + (cf_head_elb_one_weakened_budget)) * S ((cf_new_b_elb_one_weakened_budget) + (cf_head_elb_one_weakened_budget)) + ((cf_head_elb_one_weakened_budget) + (cf_head_elb_one_weakened_budget)))) * S ((cf_new_a_elb_one_weakened_budget) + (((cf_new_b_elb_one_weakened_budget) + (cf_head_elb_one_weakened_budget)) * S ((cf_new_b_elb_one_weakened_budget) + (cf_head_elb_one_weakened_budget)) + ((cf_head_elb_one_weakened_budget) + (cf_head_elb_one_weakened_budget)))) + ((((cf_new_b_elb_one_weakened_budget) + (cf_head_elb_one_weakened_budget)) * S ((cf_new_b_elb_one_weakened_budget) + (cf_head_elb_one_weakened_budget)) + ((cf_head_elb_one_weakened_budget) + (cf_head_elb_one_weakened_budget))) + (((cf_new_b_elb_one_weakened_budget) + (cf_head_elb_one_weakened_budget)) * S ((cf_new_b_elb_one_weakened_budget) + (cf_head_elb_one_weakened_budget)) + ((cf_head_elb_one_weakened_budget) + (cf_head_elb_one_weakened_budget))))))) /\ (cf_new_b_elb_one_weakened_budget = cf_old_a_elb_one_weakened_budget /\ (cf_new_a_elb_one_weakened_budget = cf_new_b_elb_one_weakened_budget * cf_quotient_elb_one_weakened_budget + cf_old_b_elb_one_weakened_budget /\ ((exists ff_lt_cf_elb_one_weakened_budget_remainder. ff_lt_cf_elb_one_weakened_budget_remainder + S cf_old_b_elb_one_weakened_budget = cf_new_b_elb_one_weakened_budget) /\ (cf_head_elb_one_weakened_budget = S ((cf_quotient_elb_one_weakened_budget + cf_tail_elb_one_weakened_budget) * S (cf_quotient_elb_one_weakened_budget + cf_tail_elb_one_weakened_budget) + (cf_tail_elb_one_weakened_budget + cf_tail_elb_one_weakened_budget))))))))))) /\ exists elb_gap_one_weakened. elb_gap_one_weakened + elb_steps_one_weakened = (S (S (n + n))))
  65. 0065specialize euclidean_log_budget_weaken a
  66. 0066specialize euclidean_log_budget_weaken b
  67. 0067specialize euclidean_log_budget_weaken (S (n + n))
  68. 0068apply euclidean_log_budget_weaken
  69. 0069exact hfirst_budget
  70. 0070specialize euclidean_log_budget_successor_power a
  71. 0071specialize euclidean_log_budget_successor_power b
  72. 0072specialize euclidean_log_budget_successor_power n
  73. 0073apply euclidean_log_budget_successor_power
  74. 0074exact hweakened
  75. 0075cases zero_or_succ_right
  76. 0076have hnonzero : ~(x2 = 0)
  77. 0077intro hzero
  78. 0078apply PA1
  79. 0079trans x2
  80. 0080symm
  81. 0081exact zero_or_succ_right_witness
  82. 0082exact hzero
  83. 0083specialize division_remainder_exists x2
  84. 0084specialize division_remainder_exists b
  85. 0085have hsecond : exists Q t. ((b = x2 * Q + t /\ (exists ff_lt_ec_elb_induction_second_division. ff_lt_ec_elb_induction_second_division + S t = x2)))
  86. 0086apply division_remainder_exists
  87. 0087exact hnonzero
  88. 0088cases hsecond
  89. 0089cases hsecond_witness
  90. 0090have hhalf : exists gap. gap + S (x5 + x5) = b
  91. 0091specialize euclidean_two_step_halving a
  92. 0092specialize euclidean_two_step_halving b
  93. 0093specialize euclidean_two_step_halving x1
  94. 0094specialize euclidean_two_step_halving x2
  95. 0095specialize euclidean_two_step_halving x4
  96. 0096specialize euclidean_two_step_halving x5
  97. 0097apply euclidean_two_step_halving
  98. 0098exact hfirst_witness_witness
  99. 0099exact hsecond_witness_witness
  100. 0100have hupper : exists gap. gap + S b = x + x
  101. 0101rewrite hdouble at hbelow
  102. 0102exact hbelow
  103. 0103have hdrop : exists gap. gap + S x5 = x
  104. 0104specialize euclidean_log_halving_power_drop b
  105. 0105specialize euclidean_log_halving_power_drop x5
  106. 0106specialize euclidean_log_halving_power_drop x
  107. 0107apply euclidean_log_halving_power_drop
  108. 0108exact hhalf
  109. 0109exact hupper
  110. 0110specialize IH x
  111. 0111have hbounded : forall b. (exists gap. gap + S b = x) -> forall a. (exists elb_list_ih_bounded elb_history_ih_bounded elb_scale_ih_bounded elb_steps_ih_bounded. ((exists cf_gcd_elb_ih_bounded_budget. ((((exists ff_h_cf_elb_ih_bounded_budget_initial_state. ff_h_cf_elb_ih_bounded_budget_initial_state + S (((cf_gcd_elb_ih_bounded_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_ih_bounded_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * elb_scale_ih_bounded)) /\ exists ff_q_cf_elb_ih_bounded_budget_initial_state. elb_history_ih_bounded = ff_q_cf_elb_ih_bounded_budget_initial_state * S ((S (0)) * elb_scale_ih_bounded) + (((cf_gcd_elb_ih_bounded_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_ih_bounded_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))))) /\ ((((exists ff_h_cf_elb_ih_bounded_budget_terminal_state. ff_h_cf_elb_ih_bounded_budget_terminal_state + S (((a) + (((b) + (elb_list_ih_bounded)) * S ((b) + (elb_list_ih_bounded)) + ((elb_list_ih_bounded) + (elb_list_ih_bounded)))) * S ((a) + (((b) + (elb_list_ih_bounded)) * S ((b) + (elb_list_ih_bounded)) + ((elb_list_ih_bounded) + (elb_list_ih_bounded)))) + ((((b) + (elb_list_ih_bounded)) * S ((b) + (elb_list_ih_bounded)) + ((elb_list_ih_bounded) + (elb_list_ih_bounded))) + (((b) + (elb_list_ih_bounded)) * S ((b) + (elb_list_ih_bounded)) + ((elb_list_ih_bounded) + (elb_list_ih_bounded))))) = S ((S (elb_steps_ih_bounded)) * elb_scale_ih_bounded)) /\ exists ff_q_cf_elb_ih_bounded_budget_terminal_state. elb_history_ih_bounded = ff_q_cf_elb_ih_bounded_budget_terminal_state * S ((S (elb_steps_ih_bounded)) * elb_scale_ih_bounded) + (((a) + (((b) + (elb_list_ih_bounded)) * S ((b) + (elb_list_ih_bounded)) + ((elb_list_ih_bounded) + (elb_list_ih_bounded)))) * S ((a) + (((b) + (elb_list_ih_bounded)) * S ((b) + (elb_list_ih_bounded)) + ((elb_list_ih_bounded) + (elb_list_ih_bounded)))) + ((((b) + (elb_list_ih_bounded)) * S ((b) + (elb_list_ih_bounded)) + ((elb_list_ih_bounded) + (elb_list_ih_bounded))) + (((b) + (elb_list_ih_bounded)) * S ((b) + (elb_list_ih_bounded)) + ((elb_list_ih_bounded) + (elb_list_ih_bounded))))))) /\ forall cf_index_elb_ih_bounded_budget. (exists ff_lt_cf_elb_ih_bounded_budget_index. ff_lt_cf_elb_ih_bounded_budget_index + S cf_index_elb_ih_bounded_budget = elb_steps_ih_bounded) -> exists cf_old_a_elb_ih_bounded_budget cf_old_b_elb_ih_bounded_budget cf_tail_elb_ih_bounded_budget cf_new_a_elb_ih_bounded_budget cf_new_b_elb_ih_bounded_budget cf_head_elb_ih_bounded_budget cf_quotient_elb_ih_bounded_budget. ((((exists ff_h_cf_elb_ih_bounded_budget_previous_state. ff_h_cf_elb_ih_bounded_budget_previous_state + S (((cf_old_a_elb_ih_bounded_budget) + (((cf_old_b_elb_ih_bounded_budget) + (cf_tail_elb_ih_bounded_budget)) * S ((cf_old_b_elb_ih_bounded_budget) + (cf_tail_elb_ih_bounded_budget)) + ((cf_tail_elb_ih_bounded_budget) + (cf_tail_elb_ih_bounded_budget)))) * S ((cf_old_a_elb_ih_bounded_budget) + (((cf_old_b_elb_ih_bounded_budget) + (cf_tail_elb_ih_bounded_budget)) * S ((cf_old_b_elb_ih_bounded_budget) + (cf_tail_elb_ih_bounded_budget)) + ((cf_tail_elb_ih_bounded_budget) + (cf_tail_elb_ih_bounded_budget)))) + ((((cf_old_b_elb_ih_bounded_budget) + (cf_tail_elb_ih_bounded_budget)) * S ((cf_old_b_elb_ih_bounded_budget) + (cf_tail_elb_ih_bounded_budget)) + ((cf_tail_elb_ih_bounded_budget) + (cf_tail_elb_ih_bounded_budget))) + (((cf_old_b_elb_ih_bounded_budget) + (cf_tail_elb_ih_bounded_budget)) * S ((cf_old_b_elb_ih_bounded_budget) + (cf_tail_elb_ih_bounded_budget)) + ((cf_tail_elb_ih_bounded_budget) + (cf_tail_elb_ih_bounded_budget))))) = S ((S (cf_index_elb_ih_bounded_budget)) * elb_scale_ih_bounded)) /\ exists ff_q_cf_elb_ih_bounded_budget_previous_state. elb_history_ih_bounded = ff_q_cf_elb_ih_bounded_budget_previous_state * S ((S (cf_index_elb_ih_bounded_budget)) * elb_scale_ih_bounded) + (((cf_old_a_elb_ih_bounded_budget) + (((cf_old_b_elb_ih_bounded_budget) + (cf_tail_elb_ih_bounded_budget)) * S ((cf_old_b_elb_ih_bounded_budget) + (cf_tail_elb_ih_bounded_budget)) + ((cf_tail_elb_ih_bounded_budget) + (cf_tail_elb_ih_bounded_budget)))) * S ((cf_old_a_elb_ih_bounded_budget) + (((cf_old_b_elb_ih_bounded_budget) + (cf_tail_elb_ih_bounded_budget)) * S ((cf_old_b_elb_ih_bounded_budget) + (cf_tail_elb_ih_bounded_budget)) + ((cf_tail_elb_ih_bounded_budget) + (cf_tail_elb_ih_bounded_budget)))) + ((((cf_old_b_elb_ih_bounded_budget) + (cf_tail_elb_ih_bounded_budget)) * S ((cf_old_b_elb_ih_bounded_budget) + (cf_tail_elb_ih_bounded_budget)) + ((cf_tail_elb_ih_bounded_budget) + (cf_tail_elb_ih_bounded_budget))) + (((cf_old_b_elb_ih_bounded_budget) + (cf_tail_elb_ih_bounded_budget)) * S ((cf_old_b_elb_ih_bounded_budget) + (cf_tail_elb_ih_bounded_budget)) + ((cf_tail_elb_ih_bounded_budget) + (cf_tail_elb_ih_bounded_budget))))))) /\ ((((exists ff_h_cf_elb_ih_bounded_budget_following_state. ff_h_cf_elb_ih_bounded_budget_following_state + S (((cf_new_a_elb_ih_bounded_budget) + (((cf_new_b_elb_ih_bounded_budget) + (cf_head_elb_ih_bounded_budget)) * S ((cf_new_b_elb_ih_bounded_budget) + (cf_head_elb_ih_bounded_budget)) + ((cf_head_elb_ih_bounded_budget) + (cf_head_elb_ih_bounded_budget)))) * S ((cf_new_a_elb_ih_bounded_budget) + (((cf_new_b_elb_ih_bounded_budget) + (cf_head_elb_ih_bounded_budget)) * S ((cf_new_b_elb_ih_bounded_budget) + (cf_head_elb_ih_bounded_budget)) + ((cf_head_elb_ih_bounded_budget) + (cf_head_elb_ih_bounded_budget)))) + ((((cf_new_b_elb_ih_bounded_budget) + (cf_head_elb_ih_bounded_budget)) * S ((cf_new_b_elb_ih_bounded_budget) + (cf_head_elb_ih_bounded_budget)) + ((cf_head_elb_ih_bounded_budget) + (cf_head_elb_ih_bounded_budget))) + (((cf_new_b_elb_ih_bounded_budget) + (cf_head_elb_ih_bounded_budget)) * S ((cf_new_b_elb_ih_bounded_budget) + (cf_head_elb_ih_bounded_budget)) + ((cf_head_elb_ih_bounded_budget) + (cf_head_elb_ih_bounded_budget))))) = S ((S (S cf_index_elb_ih_bounded_budget)) * elb_scale_ih_bounded)) /\ exists ff_q_cf_elb_ih_bounded_budget_following_state. elb_history_ih_bounded = ff_q_cf_elb_ih_bounded_budget_following_state * S ((S (S cf_index_elb_ih_bounded_budget)) * elb_scale_ih_bounded) + (((cf_new_a_elb_ih_bounded_budget) + (((cf_new_b_elb_ih_bounded_budget) + (cf_head_elb_ih_bounded_budget)) * S ((cf_new_b_elb_ih_bounded_budget) + (cf_head_elb_ih_bounded_budget)) + ((cf_head_elb_ih_bounded_budget) + (cf_head_elb_ih_bounded_budget)))) * S ((cf_new_a_elb_ih_bounded_budget) + (((cf_new_b_elb_ih_bounded_budget) + (cf_head_elb_ih_bounded_budget)) * S ((cf_new_b_elb_ih_bounded_budget) + (cf_head_elb_ih_bounded_budget)) + ((cf_head_elb_ih_bounded_budget) + (cf_head_elb_ih_bounded_budget)))) + ((((cf_new_b_elb_ih_bounded_budget) + (cf_head_elb_ih_bounded_budget)) * S ((cf_new_b_elb_ih_bounded_budget) + (cf_head_elb_ih_bounded_budget)) + ((cf_head_elb_ih_bounded_budget) + (cf_head_elb_ih_bounded_budget))) + (((cf_new_b_elb_ih_bounded_budget) + (cf_head_elb_ih_bounded_budget)) * S ((cf_new_b_elb_ih_bounded_budget) + (cf_head_elb_ih_bounded_budget)) + ((cf_head_elb_ih_bounded_budget) + (cf_head_elb_ih_bounded_budget))))))) /\ (cf_new_b_elb_ih_bounded_budget = cf_old_a_elb_ih_bounded_budget /\ (cf_new_a_elb_ih_bounded_budget = cf_new_b_elb_ih_bounded_budget * cf_quotient_elb_ih_bounded_budget + cf_old_b_elb_ih_bounded_budget /\ ((exists ff_lt_cf_elb_ih_bounded_budget_remainder. ff_lt_cf_elb_ih_bounded_budget_remainder + S cf_old_b_elb_ih_bounded_budget = cf_new_b_elb_ih_bounded_budget) /\ (cf_head_elb_ih_bounded_budget = S ((cf_quotient_elb_ih_bounded_budget + cf_tail_elb_ih_bounded_budget) * S (cf_quotient_elb_ih_bounded_budget + cf_tail_elb_ih_bounded_budget) + (cf_tail_elb_ih_bounded_budget + cf_tail_elb_ih_bounded_budget))))))))))) /\ exists elb_gap_ih_bounded. elb_gap_ih_bounded + elb_steps_ih_bounded = ((n + n))))
  112. 0112apply IH
  113. 0113exact binary_power_two_exists_witness
  114. 0114specialize hbounded x5
  115. 0115have hall : forall z. (exists elb_list_ih_all elb_history_ih_all elb_scale_ih_all elb_steps_ih_all. ((exists cf_gcd_elb_ih_all_budget. ((((exists ff_h_cf_elb_ih_all_budget_initial_state. ff_h_cf_elb_ih_all_budget_initial_state + S (((cf_gcd_elb_ih_all_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_ih_all_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * elb_scale_ih_all)) /\ exists ff_q_cf_elb_ih_all_budget_initial_state. elb_history_ih_all = ff_q_cf_elb_ih_all_budget_initial_state * S ((S (0)) * elb_scale_ih_all) + (((cf_gcd_elb_ih_all_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_ih_all_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))))) /\ ((((exists ff_h_cf_elb_ih_all_budget_terminal_state. ff_h_cf_elb_ih_all_budget_terminal_state + S (((z) + (((x5) + (elb_list_ih_all)) * S ((x5) + (elb_list_ih_all)) + ((elb_list_ih_all) + (elb_list_ih_all)))) * S ((z) + (((x5) + (elb_list_ih_all)) * S ((x5) + (elb_list_ih_all)) + ((elb_list_ih_all) + (elb_list_ih_all)))) + ((((x5) + (elb_list_ih_all)) * S ((x5) + (elb_list_ih_all)) + ((elb_list_ih_all) + (elb_list_ih_all))) + (((x5) + (elb_list_ih_all)) * S ((x5) + (elb_list_ih_all)) + ((elb_list_ih_all) + (elb_list_ih_all))))) = S ((S (elb_steps_ih_all)) * elb_scale_ih_all)) /\ exists ff_q_cf_elb_ih_all_budget_terminal_state. elb_history_ih_all = ff_q_cf_elb_ih_all_budget_terminal_state * S ((S (elb_steps_ih_all)) * elb_scale_ih_all) + (((z) + (((x5) + (elb_list_ih_all)) * S ((x5) + (elb_list_ih_all)) + ((elb_list_ih_all) + (elb_list_ih_all)))) * S ((z) + (((x5) + (elb_list_ih_all)) * S ((x5) + (elb_list_ih_all)) + ((elb_list_ih_all) + (elb_list_ih_all)))) + ((((x5) + (elb_list_ih_all)) * S ((x5) + (elb_list_ih_all)) + ((elb_list_ih_all) + (elb_list_ih_all))) + (((x5) + (elb_list_ih_all)) * S ((x5) + (elb_list_ih_all)) + ((elb_list_ih_all) + (elb_list_ih_all))))))) /\ forall cf_index_elb_ih_all_budget. (exists ff_lt_cf_elb_ih_all_budget_index. ff_lt_cf_elb_ih_all_budget_index + S cf_index_elb_ih_all_budget = elb_steps_ih_all) -> exists cf_old_a_elb_ih_all_budget cf_old_b_elb_ih_all_budget cf_tail_elb_ih_all_budget cf_new_a_elb_ih_all_budget cf_new_b_elb_ih_all_budget cf_head_elb_ih_all_budget cf_quotient_elb_ih_all_budget. ((((exists ff_h_cf_elb_ih_all_budget_previous_state. ff_h_cf_elb_ih_all_budget_previous_state + S (((cf_old_a_elb_ih_all_budget) + (((cf_old_b_elb_ih_all_budget) + (cf_tail_elb_ih_all_budget)) * S ((cf_old_b_elb_ih_all_budget) + (cf_tail_elb_ih_all_budget)) + ((cf_tail_elb_ih_all_budget) + (cf_tail_elb_ih_all_budget)))) * S ((cf_old_a_elb_ih_all_budget) + (((cf_old_b_elb_ih_all_budget) + (cf_tail_elb_ih_all_budget)) * S ((cf_old_b_elb_ih_all_budget) + (cf_tail_elb_ih_all_budget)) + ((cf_tail_elb_ih_all_budget) + (cf_tail_elb_ih_all_budget)))) + ((((cf_old_b_elb_ih_all_budget) + (cf_tail_elb_ih_all_budget)) * S ((cf_old_b_elb_ih_all_budget) + (cf_tail_elb_ih_all_budget)) + ((cf_tail_elb_ih_all_budget) + (cf_tail_elb_ih_all_budget))) + (((cf_old_b_elb_ih_all_budget) + (cf_tail_elb_ih_all_budget)) * S ((cf_old_b_elb_ih_all_budget) + (cf_tail_elb_ih_all_budget)) + ((cf_tail_elb_ih_all_budget) + (cf_tail_elb_ih_all_budget))))) = S ((S (cf_index_elb_ih_all_budget)) * elb_scale_ih_all)) /\ exists ff_q_cf_elb_ih_all_budget_previous_state. elb_history_ih_all = ff_q_cf_elb_ih_all_budget_previous_state * S ((S (cf_index_elb_ih_all_budget)) * elb_scale_ih_all) + (((cf_old_a_elb_ih_all_budget) + (((cf_old_b_elb_ih_all_budget) + (cf_tail_elb_ih_all_budget)) * S ((cf_old_b_elb_ih_all_budget) + (cf_tail_elb_ih_all_budget)) + ((cf_tail_elb_ih_all_budget) + (cf_tail_elb_ih_all_budget)))) * S ((cf_old_a_elb_ih_all_budget) + (((cf_old_b_elb_ih_all_budget) + (cf_tail_elb_ih_all_budget)) * S ((cf_old_b_elb_ih_all_budget) + (cf_tail_elb_ih_all_budget)) + ((cf_tail_elb_ih_all_budget) + (cf_tail_elb_ih_all_budget)))) + ((((cf_old_b_elb_ih_all_budget) + (cf_tail_elb_ih_all_budget)) * S ((cf_old_b_elb_ih_all_budget) + (cf_tail_elb_ih_all_budget)) + ((cf_tail_elb_ih_all_budget) + (cf_tail_elb_ih_all_budget))) + (((cf_old_b_elb_ih_all_budget) + (cf_tail_elb_ih_all_budget)) * S ((cf_old_b_elb_ih_all_budget) + (cf_tail_elb_ih_all_budget)) + ((cf_tail_elb_ih_all_budget) + (cf_tail_elb_ih_all_budget))))))) /\ ((((exists ff_h_cf_elb_ih_all_budget_following_state. ff_h_cf_elb_ih_all_budget_following_state + S (((cf_new_a_elb_ih_all_budget) + (((cf_new_b_elb_ih_all_budget) + (cf_head_elb_ih_all_budget)) * S ((cf_new_b_elb_ih_all_budget) + (cf_head_elb_ih_all_budget)) + ((cf_head_elb_ih_all_budget) + (cf_head_elb_ih_all_budget)))) * S ((cf_new_a_elb_ih_all_budget) + (((cf_new_b_elb_ih_all_budget) + (cf_head_elb_ih_all_budget)) * S ((cf_new_b_elb_ih_all_budget) + (cf_head_elb_ih_all_budget)) + ((cf_head_elb_ih_all_budget) + (cf_head_elb_ih_all_budget)))) + ((((cf_new_b_elb_ih_all_budget) + (cf_head_elb_ih_all_budget)) * S ((cf_new_b_elb_ih_all_budget) + (cf_head_elb_ih_all_budget)) + ((cf_head_elb_ih_all_budget) + (cf_head_elb_ih_all_budget))) + (((cf_new_b_elb_ih_all_budget) + (cf_head_elb_ih_all_budget)) * S ((cf_new_b_elb_ih_all_budget) + (cf_head_elb_ih_all_budget)) + ((cf_head_elb_ih_all_budget) + (cf_head_elb_ih_all_budget))))) = S ((S (S cf_index_elb_ih_all_budget)) * elb_scale_ih_all)) /\ exists ff_q_cf_elb_ih_all_budget_following_state. elb_history_ih_all = ff_q_cf_elb_ih_all_budget_following_state * S ((S (S cf_index_elb_ih_all_budget)) * elb_scale_ih_all) + (((cf_new_a_elb_ih_all_budget) + (((cf_new_b_elb_ih_all_budget) + (cf_head_elb_ih_all_budget)) * S ((cf_new_b_elb_ih_all_budget) + (cf_head_elb_ih_all_budget)) + ((cf_head_elb_ih_all_budget) + (cf_head_elb_ih_all_budget)))) * S ((cf_new_a_elb_ih_all_budget) + (((cf_new_b_elb_ih_all_budget) + (cf_head_elb_ih_all_budget)) * S ((cf_new_b_elb_ih_all_budget) + (cf_head_elb_ih_all_budget)) + ((cf_head_elb_ih_all_budget) + (cf_head_elb_ih_all_budget)))) + ((((cf_new_b_elb_ih_all_budget) + (cf_head_elb_ih_all_budget)) * S ((cf_new_b_elb_ih_all_budget) + (cf_head_elb_ih_all_budget)) + ((cf_head_elb_ih_all_budget) + (cf_head_elb_ih_all_budget))) + (((cf_new_b_elb_ih_all_budget) + (cf_head_elb_ih_all_budget)) * S ((cf_new_b_elb_ih_all_budget) + (cf_head_elb_ih_all_budget)) + ((cf_head_elb_ih_all_budget) + (cf_head_elb_ih_all_budget))))))) /\ (cf_new_b_elb_ih_all_budget = cf_old_a_elb_ih_all_budget /\ (cf_new_a_elb_ih_all_budget = cf_new_b_elb_ih_all_budget * cf_quotient_elb_ih_all_budget + cf_old_b_elb_ih_all_budget /\ ((exists ff_lt_cf_elb_ih_all_budget_remainder. ff_lt_cf_elb_ih_all_budget_remainder + S cf_old_b_elb_ih_all_budget = cf_new_b_elb_ih_all_budget) /\ (cf_head_elb_ih_all_budget = S ((cf_quotient_elb_ih_all_budget + cf_tail_elb_ih_all_budget) * S (cf_quotient_elb_ih_all_budget + cf_tail_elb_ih_all_budget) + (cf_tail_elb_ih_all_budget + cf_tail_elb_ih_all_budget))))))))))) /\ exists elb_gap_ih_all. elb_gap_ih_all + elb_steps_ih_all = ((n + n))))
  116. 0116apply hbounded
  117. 0117exact hdrop
  118. 0118specialize hall x2
  119. 0119have htwice : exists elb_list_twice_budget elb_history_twice_budget elb_scale_twice_budget elb_steps_twice_budget. ((exists cf_gcd_elb_twice_budget_budget. ((((exists ff_h_cf_elb_twice_budget_budget_initial_state. ff_h_cf_elb_twice_budget_budget_initial_state + S (((cf_gcd_elb_twice_budget_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_twice_budget_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * elb_scale_twice_budget)) /\ exists ff_q_cf_elb_twice_budget_budget_initial_state. elb_history_twice_budget = ff_q_cf_elb_twice_budget_budget_initial_state * S ((S (0)) * elb_scale_twice_budget) + (((cf_gcd_elb_twice_budget_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_twice_budget_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))))) /\ ((((exists ff_h_cf_elb_twice_budget_budget_terminal_state. ff_h_cf_elb_twice_budget_budget_terminal_state + S (((a) + (((b) + (elb_list_twice_budget)) * S ((b) + (elb_list_twice_budget)) + ((elb_list_twice_budget) + (elb_list_twice_budget)))) * S ((a) + (((b) + (elb_list_twice_budget)) * S ((b) + (elb_list_twice_budget)) + ((elb_list_twice_budget) + (elb_list_twice_budget)))) + ((((b) + (elb_list_twice_budget)) * S ((b) + (elb_list_twice_budget)) + ((elb_list_twice_budget) + (elb_list_twice_budget))) + (((b) + (elb_list_twice_budget)) * S ((b) + (elb_list_twice_budget)) + ((elb_list_twice_budget) + (elb_list_twice_budget))))) = S ((S (elb_steps_twice_budget)) * elb_scale_twice_budget)) /\ exists ff_q_cf_elb_twice_budget_budget_terminal_state. elb_history_twice_budget = ff_q_cf_elb_twice_budget_budget_terminal_state * S ((S (elb_steps_twice_budget)) * elb_scale_twice_budget) + (((a) + (((b) + (elb_list_twice_budget)) * S ((b) + (elb_list_twice_budget)) + ((elb_list_twice_budget) + (elb_list_twice_budget)))) * S ((a) + (((b) + (elb_list_twice_budget)) * S ((b) + (elb_list_twice_budget)) + ((elb_list_twice_budget) + (elb_list_twice_budget)))) + ((((b) + (elb_list_twice_budget)) * S ((b) + (elb_list_twice_budget)) + ((elb_list_twice_budget) + (elb_list_twice_budget))) + (((b) + (elb_list_twice_budget)) * S ((b) + (elb_list_twice_budget)) + ((elb_list_twice_budget) + (elb_list_twice_budget))))))) /\ forall cf_index_elb_twice_budget_budget. (exists ff_lt_cf_elb_twice_budget_budget_index. ff_lt_cf_elb_twice_budget_budget_index + S cf_index_elb_twice_budget_budget = elb_steps_twice_budget) -> exists cf_old_a_elb_twice_budget_budget cf_old_b_elb_twice_budget_budget cf_tail_elb_twice_budget_budget cf_new_a_elb_twice_budget_budget cf_new_b_elb_twice_budget_budget cf_head_elb_twice_budget_budget cf_quotient_elb_twice_budget_budget. ((((exists ff_h_cf_elb_twice_budget_budget_previous_state. ff_h_cf_elb_twice_budget_budget_previous_state + S (((cf_old_a_elb_twice_budget_budget) + (((cf_old_b_elb_twice_budget_budget) + (cf_tail_elb_twice_budget_budget)) * S ((cf_old_b_elb_twice_budget_budget) + (cf_tail_elb_twice_budget_budget)) + ((cf_tail_elb_twice_budget_budget) + (cf_tail_elb_twice_budget_budget)))) * S ((cf_old_a_elb_twice_budget_budget) + (((cf_old_b_elb_twice_budget_budget) + (cf_tail_elb_twice_budget_budget)) * S ((cf_old_b_elb_twice_budget_budget) + (cf_tail_elb_twice_budget_budget)) + ((cf_tail_elb_twice_budget_budget) + (cf_tail_elb_twice_budget_budget)))) + ((((cf_old_b_elb_twice_budget_budget) + (cf_tail_elb_twice_budget_budget)) * S ((cf_old_b_elb_twice_budget_budget) + (cf_tail_elb_twice_budget_budget)) + ((cf_tail_elb_twice_budget_budget) + (cf_tail_elb_twice_budget_budget))) + (((cf_old_b_elb_twice_budget_budget) + (cf_tail_elb_twice_budget_budget)) * S ((cf_old_b_elb_twice_budget_budget) + (cf_tail_elb_twice_budget_budget)) + ((cf_tail_elb_twice_budget_budget) + (cf_tail_elb_twice_budget_budget))))) = S ((S (cf_index_elb_twice_budget_budget)) * elb_scale_twice_budget)) /\ exists ff_q_cf_elb_twice_budget_budget_previous_state. elb_history_twice_budget = ff_q_cf_elb_twice_budget_budget_previous_state * S ((S (cf_index_elb_twice_budget_budget)) * elb_scale_twice_budget) + (((cf_old_a_elb_twice_budget_budget) + (((cf_old_b_elb_twice_budget_budget) + (cf_tail_elb_twice_budget_budget)) * S ((cf_old_b_elb_twice_budget_budget) + (cf_tail_elb_twice_budget_budget)) + ((cf_tail_elb_twice_budget_budget) + (cf_tail_elb_twice_budget_budget)))) * S ((cf_old_a_elb_twice_budget_budget) + (((cf_old_b_elb_twice_budget_budget) + (cf_tail_elb_twice_budget_budget)) * S ((cf_old_b_elb_twice_budget_budget) + (cf_tail_elb_twice_budget_budget)) + ((cf_tail_elb_twice_budget_budget) + (cf_tail_elb_twice_budget_budget)))) + ((((cf_old_b_elb_twice_budget_budget) + (cf_tail_elb_twice_budget_budget)) * S ((cf_old_b_elb_twice_budget_budget) + (cf_tail_elb_twice_budget_budget)) + ((cf_tail_elb_twice_budget_budget) + (cf_tail_elb_twice_budget_budget))) + (((cf_old_b_elb_twice_budget_budget) + (cf_tail_elb_twice_budget_budget)) * S ((cf_old_b_elb_twice_budget_budget) + (cf_tail_elb_twice_budget_budget)) + ((cf_tail_elb_twice_budget_budget) + (cf_tail_elb_twice_budget_budget))))))) /\ ((((exists ff_h_cf_elb_twice_budget_budget_following_state. ff_h_cf_elb_twice_budget_budget_following_state + S (((cf_new_a_elb_twice_budget_budget) + (((cf_new_b_elb_twice_budget_budget) + (cf_head_elb_twice_budget_budget)) * S ((cf_new_b_elb_twice_budget_budget) + (cf_head_elb_twice_budget_budget)) + ((cf_head_elb_twice_budget_budget) + (cf_head_elb_twice_budget_budget)))) * S ((cf_new_a_elb_twice_budget_budget) + (((cf_new_b_elb_twice_budget_budget) + (cf_head_elb_twice_budget_budget)) * S ((cf_new_b_elb_twice_budget_budget) + (cf_head_elb_twice_budget_budget)) + ((cf_head_elb_twice_budget_budget) + (cf_head_elb_twice_budget_budget)))) + ((((cf_new_b_elb_twice_budget_budget) + (cf_head_elb_twice_budget_budget)) * S ((cf_new_b_elb_twice_budget_budget) + (cf_head_elb_twice_budget_budget)) + ((cf_head_elb_twice_budget_budget) + (cf_head_elb_twice_budget_budget))) + (((cf_new_b_elb_twice_budget_budget) + (cf_head_elb_twice_budget_budget)) * S ((cf_new_b_elb_twice_budget_budget) + (cf_head_elb_twice_budget_budget)) + ((cf_head_elb_twice_budget_budget) + (cf_head_elb_twice_budget_budget))))) = S ((S (S cf_index_elb_twice_budget_budget)) * elb_scale_twice_budget)) /\ exists ff_q_cf_elb_twice_budget_budget_following_state. elb_history_twice_budget = ff_q_cf_elb_twice_budget_budget_following_state * S ((S (S cf_index_elb_twice_budget_budget)) * elb_scale_twice_budget) + (((cf_new_a_elb_twice_budget_budget) + (((cf_new_b_elb_twice_budget_budget) + (cf_head_elb_twice_budget_budget)) * S ((cf_new_b_elb_twice_budget_budget) + (cf_head_elb_twice_budget_budget)) + ((cf_head_elb_twice_budget_budget) + (cf_head_elb_twice_budget_budget)))) * S ((cf_new_a_elb_twice_budget_budget) + (((cf_new_b_elb_twice_budget_budget) + (cf_head_elb_twice_budget_budget)) * S ((cf_new_b_elb_twice_budget_budget) + (cf_head_elb_twice_budget_budget)) + ((cf_head_elb_twice_budget_budget) + (cf_head_elb_twice_budget_budget)))) + ((((cf_new_b_elb_twice_budget_budget) + (cf_head_elb_twice_budget_budget)) * S ((cf_new_b_elb_twice_budget_budget) + (cf_head_elb_twice_budget_budget)) + ((cf_head_elb_twice_budget_budget) + (cf_head_elb_twice_budget_budget))) + (((cf_new_b_elb_twice_budget_budget) + (cf_head_elb_twice_budget_budget)) * S ((cf_new_b_elb_twice_budget_budget) + (cf_head_elb_twice_budget_budget)) + ((cf_head_elb_twice_budget_budget) + (cf_head_elb_twice_budget_budget))))))) /\ (cf_new_b_elb_twice_budget_budget = cf_old_a_elb_twice_budget_budget /\ (cf_new_a_elb_twice_budget_budget = cf_new_b_elb_twice_budget_budget * cf_quotient_elb_twice_budget_budget + cf_old_b_elb_twice_budget_budget /\ ((exists ff_lt_cf_elb_twice_budget_budget_remainder. ff_lt_cf_elb_twice_budget_budget_remainder + S cf_old_b_elb_twice_budget_budget = cf_new_b_elb_twice_budget_budget) /\ (cf_head_elb_twice_budget_budget = S ((cf_quotient_elb_twice_budget_budget + cf_tail_elb_twice_budget_budget) * S (cf_quotient_elb_twice_budget_budget + cf_tail_elb_twice_budget_budget) + (cf_tail_elb_twice_budget_budget + cf_tail_elb_twice_budget_budget))))))))))) /\ exists elb_gap_twice_budget. elb_gap_twice_budget + elb_steps_twice_budget = (S (S (n + n))))
  120. 0120specialize euclidean_log_budget_extend_twice a
  121. 0121specialize euclidean_log_budget_extend_twice b
  122. 0122specialize euclidean_log_budget_extend_twice x1
  123. 0123specialize euclidean_log_budget_extend_twice x2
  124. 0124specialize euclidean_log_budget_extend_twice x4
  125. 0125specialize euclidean_log_budget_extend_twice x5
  126. 0126specialize euclidean_log_budget_extend_twice (n + n)
  127. 0127apply euclidean_log_budget_extend_twice
  128. 0128exact hfirst_witness_witness
  129. 0129exact hsecond_witness_witness
  130. 0130exact hall
  131. 0131specialize euclidean_log_budget_successor_power a
  132. 0132specialize euclidean_log_budget_successor_power b
  133. 0133specialize euclidean_log_budget_successor_power n
  134. 0134apply euclidean_log_budget_successor_power
  135. 0135exact htwice