BA002D

cf_convergent_old_history_nonempty_head

A genuine nonempty quotient list in G071 exposes an actual Euclidean first step and an actual shorter history length.

Alpha v34 checked-use · first admitted v29 · 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 initial 0/1 convergent is included: u is natural, not necessarily positive. Comparison denominators are strictly smaller and positive. Signed competitors are represented by an arbitrary difference rp−rn. Approximation inequalities are proved from the trace, never stored as assumptions in Convergent.

Exact theorem in conservative defined notation

∀ a. ∀ b. ∀ s. ∀ h. ∀ e. ∀ L. ContinuedFractionTrace(a,b,s,h,e,L) → ¬s = 0 → ∃ x. ∃ y. ∃ z. ∃ n. L = S n ∧ (a = b · x + y ∧ (Lt(y,b) ∧ (ListCell(s,x,z) ∧ ContinuedFractionTrace(b,y,z,h,e,n))))

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

Definition DAG

ListCell(s,q,t) · 2ContinuedFractionTrace(a,b,s,u,v,ell) · 5Lt(a,b) · 2

Actual proof prerequisites

zero_or_succ · checked external prerequisitecf_convergent_old_history_length_transportcf_convergent_old_history_zero_eliminationcf_convergent_old_history_successor_elimination
Original expanded first-order statement 
forall a b s h e L. (exists cf_gcd_head_source. ((((exists ff_h_cf_head_source_initial_state. ff_h_cf_head_source_initial_state + S (((cf_gcd_head_source) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_head_source) + (((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_head_source_initial_state. h = ff_q_cf_head_source_initial_state * S ((S (0)) * e) + (((cf_gcd_head_source) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_head_source) + (((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_head_source_terminal_state. ff_h_cf_head_source_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_head_source_terminal_state. h = ff_q_cf_head_source_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_head_source. (exists ff_lt_cf_head_source_index. ff_lt_cf_head_source_index + S cf_index_head_source = L) -> exists cf_old_a_head_source cf_old_b_head_source cf_tail_head_source cf_new_a_head_source cf_new_b_head_source cf_head_head_source cf_quotient_head_source. ((((exists ff_h_cf_head_source_previous_state. ff_h_cf_head_source_previous_state + S (((cf_old_a_head_source) + (((cf_old_b_head_source) + (cf_tail_head_source)) * S ((cf_old_b_head_source) + (cf_tail_head_source)) + ((cf_tail_head_source) + (cf_tail_head_source)))) * S ((cf_old_a_head_source) + (((cf_old_b_head_source) + (cf_tail_head_source)) * S ((cf_old_b_head_source) + (cf_tail_head_source)) + ((cf_tail_head_source) + (cf_tail_head_source)))) + ((((cf_old_b_head_source) + (cf_tail_head_source)) * S ((cf_old_b_head_source) + (cf_tail_head_source)) + ((cf_tail_head_source) + (cf_tail_head_source))) + (((cf_old_b_head_source) + (cf_tail_head_source)) * S ((cf_old_b_head_source) + (cf_tail_head_source)) + ((cf_tail_head_source) + (cf_tail_head_source))))) = S ((S (cf_index_head_source)) * e)) /\ exists ff_q_cf_head_source_previous_state. h = ff_q_cf_head_source_previous_state * S ((S (cf_index_head_source)) * e) + (((cf_old_a_head_source) + (((cf_old_b_head_source) + (cf_tail_head_source)) * S ((cf_old_b_head_source) + (cf_tail_head_source)) + ((cf_tail_head_source) + (cf_tail_head_source)))) * S ((cf_old_a_head_source) + (((cf_old_b_head_source) + (cf_tail_head_source)) * S ((cf_old_b_head_source) + (cf_tail_head_source)) + ((cf_tail_head_source) + (cf_tail_head_source)))) + ((((cf_old_b_head_source) + (cf_tail_head_source)) * S ((cf_old_b_head_source) + (cf_tail_head_source)) + ((cf_tail_head_source) + (cf_tail_head_source))) + (((cf_old_b_head_source) + (cf_tail_head_source)) * S ((cf_old_b_head_source) + (cf_tail_head_source)) + ((cf_tail_head_source) + (cf_tail_head_source))))))) /\ ((((exists ff_h_cf_head_source_following_state. ff_h_cf_head_source_following_state + S (((cf_new_a_head_source) + (((cf_new_b_head_source) + (cf_head_head_source)) * S ((cf_new_b_head_source) + (cf_head_head_source)) + ((cf_head_head_source) + (cf_head_head_source)))) * S ((cf_new_a_head_source) + (((cf_new_b_head_source) + (cf_head_head_source)) * S ((cf_new_b_head_source) + (cf_head_head_source)) + ((cf_head_head_source) + (cf_head_head_source)))) + ((((cf_new_b_head_source) + (cf_head_head_source)) * S ((cf_new_b_head_source) + (cf_head_head_source)) + ((cf_head_head_source) + (cf_head_head_source))) + (((cf_new_b_head_source) + (cf_head_head_source)) * S ((cf_new_b_head_source) + (cf_head_head_source)) + ((cf_head_head_source) + (cf_head_head_source))))) = S ((S (S cf_index_head_source)) * e)) /\ exists ff_q_cf_head_source_following_state. h = ff_q_cf_head_source_following_state * S ((S (S cf_index_head_source)) * e) + (((cf_new_a_head_source) + (((cf_new_b_head_source) + (cf_head_head_source)) * S ((cf_new_b_head_source) + (cf_head_head_source)) + ((cf_head_head_source) + (cf_head_head_source)))) * S ((cf_new_a_head_source) + (((cf_new_b_head_source) + (cf_head_head_source)) * S ((cf_new_b_head_source) + (cf_head_head_source)) + ((cf_head_head_source) + (cf_head_head_source)))) + ((((cf_new_b_head_source) + (cf_head_head_source)) * S ((cf_new_b_head_source) + (cf_head_head_source)) + ((cf_head_head_source) + (cf_head_head_source))) + (((cf_new_b_head_source) + (cf_head_head_source)) * S ((cf_new_b_head_source) + (cf_head_head_source)) + ((cf_head_head_source) + (cf_head_head_source))))))) /\ (cf_new_b_head_source = cf_old_a_head_source /\ (cf_new_a_head_source = cf_new_b_head_source * cf_quotient_head_source + cf_old_b_head_source /\ ((exists ff_lt_cf_head_source_remainder. ff_lt_cf_head_source_remainder + S cf_old_b_head_source = cf_new_b_head_source) /\ (cf_head_head_source = S ((cf_quotient_head_source + cf_tail_head_source) * S (cf_quotient_head_source + cf_tail_head_source) + (cf_tail_head_source + cf_tail_head_source))))))))))) -> ~(s = 0) -> (exists cfc_q_head_result cfc_r_head_result cfc_tail_head_result cfc_length_head_result. (((L) = S cfc_length_head_result) /\ (((a) = (b) * cfc_q_head_result + cfc_r_head_result) /\ ((exists cfba_gap_head_resultbound. cfba_gap_head_resultbound + S (cfc_r_head_result) = (b)) /\ ((s = S ((cfc_q_head_result + cfc_tail_head_result) * S (cfc_q_head_result + cfc_tail_head_result) + (cfc_tail_head_result + cfc_tail_head_result))) /\ (exists cf_gcd_head_resulthistory. ((((exists ff_h_cf_head_resulthistory_initial_state. ff_h_cf_head_resulthistory_initial_state + S (((cf_gcd_head_resulthistory) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_head_resulthistory) + (((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_head_resulthistory_initial_state. h = ff_q_cf_head_resulthistory_initial_state * S ((S (0)) * e) + (((cf_gcd_head_resulthistory) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_head_resulthistory) + (((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_head_resulthistory_terminal_state. ff_h_cf_head_resulthistory_terminal_state + S (((b) + (((cfc_r_head_result) + (cfc_tail_head_result)) * S ((cfc_r_head_result) + (cfc_tail_head_result)) + ((cfc_tail_head_result) + (cfc_tail_head_result)))) * S ((b) + (((cfc_r_head_result) + (cfc_tail_head_result)) * S ((cfc_r_head_result) + (cfc_tail_head_result)) + ((cfc_tail_head_result) + (cfc_tail_head_result)))) + ((((cfc_r_head_result) + (cfc_tail_head_result)) * S ((cfc_r_head_result) + (cfc_tail_head_result)) + ((cfc_tail_head_result) + (cfc_tail_head_result))) + (((cfc_r_head_result) + (cfc_tail_head_result)) * S ((cfc_r_head_result) + (cfc_tail_head_result)) + ((cfc_tail_head_result) + (cfc_tail_head_result))))) = S ((S (cfc_length_head_result)) * e)) /\ exists ff_q_cf_head_resulthistory_terminal_state. h = ff_q_cf_head_resulthistory_terminal_state * S ((S (cfc_length_head_result)) * e) + (((b) + (((cfc_r_head_result) + (cfc_tail_head_result)) * S ((cfc_r_head_result) + (cfc_tail_head_result)) + ((cfc_tail_head_result) + (cfc_tail_head_result)))) * S ((b) + (((cfc_r_head_result) + (cfc_tail_head_result)) * S ((cfc_r_head_result) + (cfc_tail_head_result)) + ((cfc_tail_head_result) + (cfc_tail_head_result)))) + ((((cfc_r_head_result) + (cfc_tail_head_result)) * S ((cfc_r_head_result) + (cfc_tail_head_result)) + ((cfc_tail_head_result) + (cfc_tail_head_result))) + (((cfc_r_head_result) + (cfc_tail_head_result)) * S ((cfc_r_head_result) + (cfc_tail_head_result)) + ((cfc_tail_head_result) + (cfc_tail_head_result))))))) /\ forall cf_index_head_resulthistory. (exists ff_lt_cf_head_resulthistory_index. ff_lt_cf_head_resulthistory_index + S cf_index_head_resulthistory = cfc_length_head_result) -> exists cf_old_a_head_resulthistory cf_old_b_head_resulthistory cf_tail_head_resulthistory cf_new_a_head_resulthistory cf_new_b_head_resulthistory cf_head_head_resulthistory cf_quotient_head_resulthistory. ((((exists ff_h_cf_head_resulthistory_previous_state. ff_h_cf_head_resulthistory_previous_state + S (((cf_old_a_head_resulthistory) + (((cf_old_b_head_resulthistory) + (cf_tail_head_resulthistory)) * S ((cf_old_b_head_resulthistory) + (cf_tail_head_resulthistory)) + ((cf_tail_head_resulthistory) + (cf_tail_head_resulthistory)))) * S ((cf_old_a_head_resulthistory) + (((cf_old_b_head_resulthistory) + (cf_tail_head_resulthistory)) * S ((cf_old_b_head_resulthistory) + (cf_tail_head_resulthistory)) + ((cf_tail_head_resulthistory) + (cf_tail_head_resulthistory)))) + ((((cf_old_b_head_resulthistory) + (cf_tail_head_resulthistory)) * S ((cf_old_b_head_resulthistory) + (cf_tail_head_resulthistory)) + ((cf_tail_head_resulthistory) + (cf_tail_head_resulthistory))) + (((cf_old_b_head_resulthistory) + (cf_tail_head_resulthistory)) * S ((cf_old_b_head_resulthistory) + (cf_tail_head_resulthistory)) + ((cf_tail_head_resulthistory) + (cf_tail_head_resulthistory))))) = S ((S (cf_index_head_resulthistory)) * e)) /\ exists ff_q_cf_head_resulthistory_previous_state. h = ff_q_cf_head_resulthistory_previous_state * S ((S (cf_index_head_resulthistory)) * e) + (((cf_old_a_head_resulthistory) + (((cf_old_b_head_resulthistory) + (cf_tail_head_resulthistory)) * S ((cf_old_b_head_resulthistory) + (cf_tail_head_resulthistory)) + ((cf_tail_head_resulthistory) + (cf_tail_head_resulthistory)))) * S ((cf_old_a_head_resulthistory) + (((cf_old_b_head_resulthistory) + (cf_tail_head_resulthistory)) * S ((cf_old_b_head_resulthistory) + (cf_tail_head_resulthistory)) + ((cf_tail_head_resulthistory) + (cf_tail_head_resulthistory)))) + ((((cf_old_b_head_resulthistory) + (cf_tail_head_resulthistory)) * S ((cf_old_b_head_resulthistory) + (cf_tail_head_resulthistory)) + ((cf_tail_head_resulthistory) + (cf_tail_head_resulthistory))) + (((cf_old_b_head_resulthistory) + (cf_tail_head_resulthistory)) * S ((cf_old_b_head_resulthistory) + (cf_tail_head_resulthistory)) + ((cf_tail_head_resulthistory) + (cf_tail_head_resulthistory))))))) /\ ((((exists ff_h_cf_head_resulthistory_following_state. ff_h_cf_head_resulthistory_following_state + S (((cf_new_a_head_resulthistory) + (((cf_new_b_head_resulthistory) + (cf_head_head_resulthistory)) * S ((cf_new_b_head_resulthistory) + (cf_head_head_resulthistory)) + ((cf_head_head_resulthistory) + (cf_head_head_resulthistory)))) * S ((cf_new_a_head_resulthistory) + (((cf_new_b_head_resulthistory) + (cf_head_head_resulthistory)) * S ((cf_new_b_head_resulthistory) + (cf_head_head_resulthistory)) + ((cf_head_head_resulthistory) + (cf_head_head_resulthistory)))) + ((((cf_new_b_head_resulthistory) + (cf_head_head_resulthistory)) * S ((cf_new_b_head_resulthistory) + (cf_head_head_resulthistory)) + ((cf_head_head_resulthistory) + (cf_head_head_resulthistory))) + (((cf_new_b_head_resulthistory) + (cf_head_head_resulthistory)) * S ((cf_new_b_head_resulthistory) + (cf_head_head_resulthistory)) + ((cf_head_head_resulthistory) + (cf_head_head_resulthistory))))) = S ((S (S cf_index_head_resulthistory)) * e)) /\ exists ff_q_cf_head_resulthistory_following_state. h = ff_q_cf_head_resulthistory_following_state * S ((S (S cf_index_head_resulthistory)) * e) + (((cf_new_a_head_resulthistory) + (((cf_new_b_head_resulthistory) + (cf_head_head_resulthistory)) * S ((cf_new_b_head_resulthistory) + (cf_head_head_resulthistory)) + ((cf_head_head_resulthistory) + (cf_head_head_resulthistory)))) * S ((cf_new_a_head_resulthistory) + (((cf_new_b_head_resulthistory) + (cf_head_head_resulthistory)) * S ((cf_new_b_head_resulthistory) + (cf_head_head_resulthistory)) + ((cf_head_head_resulthistory) + (cf_head_head_resulthistory)))) + ((((cf_new_b_head_resulthistory) + (cf_head_head_resulthistory)) * S ((cf_new_b_head_resulthistory) + (cf_head_head_resulthistory)) + ((cf_head_head_resulthistory) + (cf_head_head_resulthistory))) + (((cf_new_b_head_resulthistory) + (cf_head_head_resulthistory)) * S ((cf_new_b_head_resulthistory) + (cf_head_head_resulthistory)) + ((cf_head_head_resulthistory) + (cf_head_head_resulthistory))))))) /\ (cf_new_b_head_resulthistory = cf_old_a_head_resulthistory /\ (cf_new_a_head_resulthistory = cf_new_b_head_resulthistory * cf_quotient_head_resulthistory + cf_old_b_head_resulthistory /\ ((exists ff_lt_cf_head_resulthistory_remainder. ff_lt_cf_head_resulthistory_remainder + S cf_old_b_head_resulthistory = cf_new_b_head_resulthistory) /\ (cf_head_head_resulthistory = S ((cf_quotient_head_resulthistory + cf_tail_head_resulthistory) * S (cf_quotient_head_resulthistory + cf_tail_head_resulthistory) + (cf_tail_head_resulthistory + cf_tail_head_resulthistory))))))))))))))))

Complete tactic proof in conservative notation

All 75 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

75 script commands · 22 reading checkpoints · 5 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 (3)
cf convergent old history length transportcf convergent old history zero eliminationcf convergent old history successor elimination
01Fix variables and assumptionsL1–8

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 ht
  8. L8
    intro hn
02Establish hlL9–11

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

  1. L9
    have hl : L = 0 \/ exists k. L = S k
  2. L10
    specialize zero_or_succ (L)
  3. L11
    apply zero_or_succ
03Separate the logical casesL12–12

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

  1. L12
    cases hl
04Establish hzL13–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply cf convergent old history length transport.

  1. L13
    have hz : ContinuedFractionTrace(a,b,s,h,e,0)Definitions: ContinuedFractionTrace(a,b,s,h,e,0)Original native command in the exact edition
  2. L14
    specialize cf_convergent_old_history_length_transport (a)
  3. L15
    specialize cf_convergent_old_history_length_transport (b)
  4. L16
    specialize cf_convergent_old_history_length_transport (s)
  5. L17
    specialize cf_convergent_old_history_length_transport (h)
  6. L18
    specialize cf_convergent_old_history_length_transport (e)
  7. L19
    specialize cf_convergent_old_history_length_transport (L)
  8. L20
    specialize cf_convergent_old_history_length_transport (0)
  9. L21
    apply cf_convergent_old_history_length_transport
  10. L22
    exact hl_left
05Use earlier factsL23–23

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

  1. L23
    exact ht
06Establish heL24–31

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply cf convergent old history zero elimination.

  1. L24
    have he : b = 0 /\ s = 0
  2. L25
    specialize cf_convergent_old_history_zero_elimination (a)
  3. L26
    specialize cf_convergent_old_history_zero_elimination (b)
  4. L27
    specialize cf_convergent_old_history_zero_elimination (s)
  5. L28
    specialize cf_convergent_old_history_zero_elimination (h)
  6. L29
    specialize cf_convergent_old_history_zero_elimination (e)
  7. L30
    apply cf_convergent_old_history_zero_elimination
  8. L31
    exact hz
07Separate the logical casesL32–33

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

  1. L32
    cases he
  2. L33
    exfalso
08Use earlier factsL34–35

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

  1. L34
    apply hn
  2. L35
    exact he_right
09Separate the logical casesL36–36

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

  1. L36
    cases hl_right
10Establish hhL37–46

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply cf convergent old history length transport.

  1. L37
    have hh : ContinuedFractionTrace(a,b,s,h,e,S x)Definitions: ContinuedFractionTrace(a,b,s,h,e,S x)Original native command in the exact edition
  2. L38
    specialize cf_convergent_old_history_length_transport (a)
  3. L39
    specialize cf_convergent_old_history_length_transport (b)
  4. L40
    specialize cf_convergent_old_history_length_transport (s)
  5. L41
    specialize cf_convergent_old_history_length_transport (h)
  6. L42
    specialize cf_convergent_old_history_length_transport (e)
  7. L43
    specialize cf_convergent_old_history_length_transport (L)
  8. L44
    specialize cf_convergent_old_history_length_transport (S x)
  9. L45
    apply cf_convergent_old_history_length_transport
  10. L46
    exact hl_right_witness
11Use earlier factsL47–47

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

  1. L47
    exact ht
12Establish hpL48–56

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply cf convergent old history successor elimination.

  1. L48
    have hp : ∃ q. ∃ r. ∃ t. a = b · q + r ∧ (Lt(r,b) ∧ (ListCell(s,q,t) ∧ ContinuedFractionTrace(b,r,t,h,e,x)))Definitions: Lt(r,b)ListCell(s,q,t)ContinuedFractionTrace(b,r,t,h,e,x)Original native command in the exact edition
  2. L49
    specialize cf_convergent_old_history_successor_elimination (a)
  3. L50
    specialize cf_convergent_old_history_successor_elimination (b)
  4. L51
    specialize cf_convergent_old_history_successor_elimination (s)
  5. L52
    specialize cf_convergent_old_history_successor_elimination (h)
  6. L53
    specialize cf_convergent_old_history_successor_elimination (e)
  7. L54
    specialize cf_convergent_old_history_successor_elimination (x)
  8. L55
    apply cf_convergent_old_history_successor_elimination
  9. L56
    exact hh
13Separate the logical casesL57–62

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

  1. L57
    cases hp
  2. L58
    cases hp_witness
  3. L59
    cases hp_witness_witness
  4. L60
    cases hp_witness_witness_witness
  5. L61
    cases hp_witness_witness_witness_right
  6. L62
    cases hp_witness_witness_witness_right_right
14Construct an explicit witnessL63–66

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

  1. L63
    exists x1
  2. L64
    exists x2
  3. L65
    exists x3
  4. L66
    exists x
15Separate the logical casesL67–67

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

  1. L67
    split
16Use earlier factsL68–68

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

  1. L68
    exact hl_right_witness
17Separate the logical casesL69–69

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

  1. L69
    split
18Use earlier factsL70–70

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

  1. L70
    exact hp_witness_witness_witness_left
19Separate the logical casesL71–71

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

  1. L71
    split
20Use earlier factsL72–72

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

  1. L72
    exact hp_witness_witness_witness_right_left
21Separate the logical casesL73–73

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

  1. L73
    split
22Use earlier factsL74–75

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

  1. L74
    exact hp_witness_witness_witness_right_right_left
  2. L75
    exact hp_witness_witness_witness_right_right_right

Library-wide reading audit

Original defined command ledger · 75 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro s
  4. 0004intro h
  5. 0005intro e
  6. 0006intro L
  7. 0007intro ht
  8. 0008intro hn
  9. 0009have hl : L = 0 \/ exists k. L = S k
  10. 0010specialize zero_or_succ (L)
  11. 0011apply zero_or_succ
  12. 0012cases hl
  13. 0013have hz : ContinuedFractionTrace(a,b,s,h,e,0)
  14. 0014specialize cf_convergent_old_history_length_transport (a)
  15. 0015specialize cf_convergent_old_history_length_transport (b)
  16. 0016specialize cf_convergent_old_history_length_transport (s)
  17. 0017specialize cf_convergent_old_history_length_transport (h)
  18. 0018specialize cf_convergent_old_history_length_transport (e)
  19. 0019specialize cf_convergent_old_history_length_transport (L)
  20. 0020specialize cf_convergent_old_history_length_transport (0)
  21. 0021apply cf_convergent_old_history_length_transport
  22. 0022exact hl_left
  23. 0023exact ht
  24. 0024have he : b = 0 /\ s = 0
  25. 0025specialize cf_convergent_old_history_zero_elimination (a)
  26. 0026specialize cf_convergent_old_history_zero_elimination (b)
  27. 0027specialize cf_convergent_old_history_zero_elimination (s)
  28. 0028specialize cf_convergent_old_history_zero_elimination (h)
  29. 0029specialize cf_convergent_old_history_zero_elimination (e)
  30. 0030apply cf_convergent_old_history_zero_elimination
  31. 0031exact hz
  32. 0032cases he
  33. 0033exfalso
  34. 0034apply hn
  35. 0035exact he_right
  36. 0036cases hl_right
  37. 0037have hh : ContinuedFractionTrace(a,b,s,h,e,S x)
  38. 0038specialize cf_convergent_old_history_length_transport (a)
  39. 0039specialize cf_convergent_old_history_length_transport (b)
  40. 0040specialize cf_convergent_old_history_length_transport (s)
  41. 0041specialize cf_convergent_old_history_length_transport (h)
  42. 0042specialize cf_convergent_old_history_length_transport (e)
  43. 0043specialize cf_convergent_old_history_length_transport (L)
  44. 0044specialize cf_convergent_old_history_length_transport (S x)
  45. 0045apply cf_convergent_old_history_length_transport
  46. 0046exact hl_right_witness
  47. 0047exact ht
  48. 0048have hp : ∃ q. ∃ r. ∃ t. a = b · q + r ∧ (Lt(r,b) ∧ (ListCell(s,q,t) ∧ ContinuedFractionTrace(b,r,t,h,e,x)))
  49. 0049specialize cf_convergent_old_history_successor_elimination (a)
  50. 0050specialize cf_convergent_old_history_successor_elimination (b)
  51. 0051specialize cf_convergent_old_history_successor_elimination (s)
  52. 0052specialize cf_convergent_old_history_successor_elimination (h)
  53. 0053specialize cf_convergent_old_history_successor_elimination (e)
  54. 0054specialize cf_convergent_old_history_successor_elimination (x)
  55. 0055apply cf_convergent_old_history_successor_elimination
  56. 0056exact hh
  57. 0057cases hp
  58. 0058cases hp_witness
  59. 0059cases hp_witness_witness
  60. 0060cases hp_witness_witness_witness
  61. 0061cases hp_witness_witness_witness_right
  62. 0062cases hp_witness_witness_witness_right_right
  63. 0063exists x1
  64. 0064exists x2
  65. 0065exists x3
  66. 0066exists x
  67. 0067split
  68. 0068exact hl_right_witness
  69. 0069split
  70. 0070exact hp_witness_witness_witness_left
  71. 0071split
  72. 0072exact hp_witness_witness_witness_right_left
  73. 0073split
  74. 0074exact hp_witness_witness_witness_right_right_left
  75. 0075exact hp_witness_witness_witness_right_right_right