BA002A

cf_convergent_old_history_successor_elimination

A complete G071 history exposes its actual first quotient, strict remainder, tagged tail, and predecessor Euclidean history.

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. ∀ k. ContinuedFractionTrace(a,b,s,h,e,S k) → ∃ x. ∃ y. ∃ z. a = b · x + y ∧ (Lt(y,b) ∧ (ListCell(s,x,z) ∧ ContinuedFractionTrace(b,y,z,h,e,k)))

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

Definition DAG

ListCell(s,q,t) · 2ContinuedFractionTrace(a,b,s,u,v,ell) · 3Lt(a,b) · 2BetaAt(b,c,i,x) · 2

Actual proof prerequisites

cf_convergent_old_history_state_uniquezero_add · checked external prerequisitelt_of_lt_of_le · checked external prerequisitele_succ_self · checked external prerequisite
Original expanded first-order statement 
forall a b s h e k. (exists cf_gcd_old_successor. ((((exists ff_h_cf_old_successor_initial_state. ff_h_cf_old_successor_initial_state + S (((cf_gcd_old_successor) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_old_successor) + (((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_old_successor_initial_state. h = ff_q_cf_old_successor_initial_state * S ((S (0)) * e) + (((cf_gcd_old_successor) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_old_successor) + (((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_old_successor_terminal_state. ff_h_cf_old_successor_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 (S k)) * e)) /\ exists ff_q_cf_old_successor_terminal_state. h = ff_q_cf_old_successor_terminal_state * S ((S (S k)) * 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_old_successor. (exists ff_lt_cf_old_successor_index. ff_lt_cf_old_successor_index + S cf_index_old_successor = S k) -> exists cf_old_a_old_successor cf_old_b_old_successor cf_tail_old_successor cf_new_a_old_successor cf_new_b_old_successor cf_head_old_successor cf_quotient_old_successor. ((((exists ff_h_cf_old_successor_previous_state. ff_h_cf_old_successor_previous_state + S (((cf_old_a_old_successor) + (((cf_old_b_old_successor) + (cf_tail_old_successor)) * S ((cf_old_b_old_successor) + (cf_tail_old_successor)) + ((cf_tail_old_successor) + (cf_tail_old_successor)))) * S ((cf_old_a_old_successor) + (((cf_old_b_old_successor) + (cf_tail_old_successor)) * S ((cf_old_b_old_successor) + (cf_tail_old_successor)) + ((cf_tail_old_successor) + (cf_tail_old_successor)))) + ((((cf_old_b_old_successor) + (cf_tail_old_successor)) * S ((cf_old_b_old_successor) + (cf_tail_old_successor)) + ((cf_tail_old_successor) + (cf_tail_old_successor))) + (((cf_old_b_old_successor) + (cf_tail_old_successor)) * S ((cf_old_b_old_successor) + (cf_tail_old_successor)) + ((cf_tail_old_successor) + (cf_tail_old_successor))))) = S ((S (cf_index_old_successor)) * e)) /\ exists ff_q_cf_old_successor_previous_state. h = ff_q_cf_old_successor_previous_state * S ((S (cf_index_old_successor)) * e) + (((cf_old_a_old_successor) + (((cf_old_b_old_successor) + (cf_tail_old_successor)) * S ((cf_old_b_old_successor) + (cf_tail_old_successor)) + ((cf_tail_old_successor) + (cf_tail_old_successor)))) * S ((cf_old_a_old_successor) + (((cf_old_b_old_successor) + (cf_tail_old_successor)) * S ((cf_old_b_old_successor) + (cf_tail_old_successor)) + ((cf_tail_old_successor) + (cf_tail_old_successor)))) + ((((cf_old_b_old_successor) + (cf_tail_old_successor)) * S ((cf_old_b_old_successor) + (cf_tail_old_successor)) + ((cf_tail_old_successor) + (cf_tail_old_successor))) + (((cf_old_b_old_successor) + (cf_tail_old_successor)) * S ((cf_old_b_old_successor) + (cf_tail_old_successor)) + ((cf_tail_old_successor) + (cf_tail_old_successor))))))) /\ ((((exists ff_h_cf_old_successor_following_state. ff_h_cf_old_successor_following_state + S (((cf_new_a_old_successor) + (((cf_new_b_old_successor) + (cf_head_old_successor)) * S ((cf_new_b_old_successor) + (cf_head_old_successor)) + ((cf_head_old_successor) + (cf_head_old_successor)))) * S ((cf_new_a_old_successor) + (((cf_new_b_old_successor) + (cf_head_old_successor)) * S ((cf_new_b_old_successor) + (cf_head_old_successor)) + ((cf_head_old_successor) + (cf_head_old_successor)))) + ((((cf_new_b_old_successor) + (cf_head_old_successor)) * S ((cf_new_b_old_successor) + (cf_head_old_successor)) + ((cf_head_old_successor) + (cf_head_old_successor))) + (((cf_new_b_old_successor) + (cf_head_old_successor)) * S ((cf_new_b_old_successor) + (cf_head_old_successor)) + ((cf_head_old_successor) + (cf_head_old_successor))))) = S ((S (S cf_index_old_successor)) * e)) /\ exists ff_q_cf_old_successor_following_state. h = ff_q_cf_old_successor_following_state * S ((S (S cf_index_old_successor)) * e) + (((cf_new_a_old_successor) + (((cf_new_b_old_successor) + (cf_head_old_successor)) * S ((cf_new_b_old_successor) + (cf_head_old_successor)) + ((cf_head_old_successor) + (cf_head_old_successor)))) * S ((cf_new_a_old_successor) + (((cf_new_b_old_successor) + (cf_head_old_successor)) * S ((cf_new_b_old_successor) + (cf_head_old_successor)) + ((cf_head_old_successor) + (cf_head_old_successor)))) + ((((cf_new_b_old_successor) + (cf_head_old_successor)) * S ((cf_new_b_old_successor) + (cf_head_old_successor)) + ((cf_head_old_successor) + (cf_head_old_successor))) + (((cf_new_b_old_successor) + (cf_head_old_successor)) * S ((cf_new_b_old_successor) + (cf_head_old_successor)) + ((cf_head_old_successor) + (cf_head_old_successor))))))) /\ (cf_new_b_old_successor = cf_old_a_old_successor /\ (cf_new_a_old_successor = cf_new_b_old_successor * cf_quotient_old_successor + cf_old_b_old_successor /\ ((exists ff_lt_cf_old_successor_remainder. ff_lt_cf_old_successor_remainder + S cf_old_b_old_successor = cf_new_b_old_successor) /\ (cf_head_old_successor = S ((cf_quotient_old_successor + cf_tail_old_successor) * S (cf_quotient_old_successor + cf_tail_old_successor) + (cf_tail_old_successor + cf_tail_old_successor))))))))))) -> exists q r t. ((a = b * q + r) /\ ((exists cfba_gap_old_predecessor_bound. cfba_gap_old_predecessor_bound + S (r) = (b)) /\ ((s = S ((q + t) * S (q + t) + (t + t))) /\ (exists cf_gcd_old_predecessor_history. ((((exists ff_h_cf_old_predecessor_history_initial_state. ff_h_cf_old_predecessor_history_initial_state + S (((cf_gcd_old_predecessor_history) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_old_predecessor_history) + (((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_old_predecessor_history_initial_state. h = ff_q_cf_old_predecessor_history_initial_state * S ((S (0)) * e) + (((cf_gcd_old_predecessor_history) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_old_predecessor_history) + (((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_old_predecessor_history_terminal_state. ff_h_cf_old_predecessor_history_terminal_state + S (((b) + (((r) + (t)) * S ((r) + (t)) + ((t) + (t)))) * S ((b) + (((r) + (t)) * S ((r) + (t)) + ((t) + (t)))) + ((((r) + (t)) * S ((r) + (t)) + ((t) + (t))) + (((r) + (t)) * S ((r) + (t)) + ((t) + (t))))) = S ((S (k)) * e)) /\ exists ff_q_cf_old_predecessor_history_terminal_state. h = ff_q_cf_old_predecessor_history_terminal_state * S ((S (k)) * e) + (((b) + (((r) + (t)) * S ((r) + (t)) + ((t) + (t)))) * S ((b) + (((r) + (t)) * S ((r) + (t)) + ((t) + (t)))) + ((((r) + (t)) * S ((r) + (t)) + ((t) + (t))) + (((r) + (t)) * S ((r) + (t)) + ((t) + (t))))))) /\ forall cf_index_old_predecessor_history. (exists ff_lt_cf_old_predecessor_history_index. ff_lt_cf_old_predecessor_history_index + S cf_index_old_predecessor_history = k) -> exists cf_old_a_old_predecessor_history cf_old_b_old_predecessor_history cf_tail_old_predecessor_history cf_new_a_old_predecessor_history cf_new_b_old_predecessor_history cf_head_old_predecessor_history cf_quotient_old_predecessor_history. ((((exists ff_h_cf_old_predecessor_history_previous_state. ff_h_cf_old_predecessor_history_previous_state + S (((cf_old_a_old_predecessor_history) + (((cf_old_b_old_predecessor_history) + (cf_tail_old_predecessor_history)) * S ((cf_old_b_old_predecessor_history) + (cf_tail_old_predecessor_history)) + ((cf_tail_old_predecessor_history) + (cf_tail_old_predecessor_history)))) * S ((cf_old_a_old_predecessor_history) + (((cf_old_b_old_predecessor_history) + (cf_tail_old_predecessor_history)) * S ((cf_old_b_old_predecessor_history) + (cf_tail_old_predecessor_history)) + ((cf_tail_old_predecessor_history) + (cf_tail_old_predecessor_history)))) + ((((cf_old_b_old_predecessor_history) + (cf_tail_old_predecessor_history)) * S ((cf_old_b_old_predecessor_history) + (cf_tail_old_predecessor_history)) + ((cf_tail_old_predecessor_history) + (cf_tail_old_predecessor_history))) + (((cf_old_b_old_predecessor_history) + (cf_tail_old_predecessor_history)) * S ((cf_old_b_old_predecessor_history) + (cf_tail_old_predecessor_history)) + ((cf_tail_old_predecessor_history) + (cf_tail_old_predecessor_history))))) = S ((S (cf_index_old_predecessor_history)) * e)) /\ exists ff_q_cf_old_predecessor_history_previous_state. h = ff_q_cf_old_predecessor_history_previous_state * S ((S (cf_index_old_predecessor_history)) * e) + (((cf_old_a_old_predecessor_history) + (((cf_old_b_old_predecessor_history) + (cf_tail_old_predecessor_history)) * S ((cf_old_b_old_predecessor_history) + (cf_tail_old_predecessor_history)) + ((cf_tail_old_predecessor_history) + (cf_tail_old_predecessor_history)))) * S ((cf_old_a_old_predecessor_history) + (((cf_old_b_old_predecessor_history) + (cf_tail_old_predecessor_history)) * S ((cf_old_b_old_predecessor_history) + (cf_tail_old_predecessor_history)) + ((cf_tail_old_predecessor_history) + (cf_tail_old_predecessor_history)))) + ((((cf_old_b_old_predecessor_history) + (cf_tail_old_predecessor_history)) * S ((cf_old_b_old_predecessor_history) + (cf_tail_old_predecessor_history)) + ((cf_tail_old_predecessor_history) + (cf_tail_old_predecessor_history))) + (((cf_old_b_old_predecessor_history) + (cf_tail_old_predecessor_history)) * S ((cf_old_b_old_predecessor_history) + (cf_tail_old_predecessor_history)) + ((cf_tail_old_predecessor_history) + (cf_tail_old_predecessor_history))))))) /\ ((((exists ff_h_cf_old_predecessor_history_following_state. ff_h_cf_old_predecessor_history_following_state + S (((cf_new_a_old_predecessor_history) + (((cf_new_b_old_predecessor_history) + (cf_head_old_predecessor_history)) * S ((cf_new_b_old_predecessor_history) + (cf_head_old_predecessor_history)) + ((cf_head_old_predecessor_history) + (cf_head_old_predecessor_history)))) * S ((cf_new_a_old_predecessor_history) + (((cf_new_b_old_predecessor_history) + (cf_head_old_predecessor_history)) * S ((cf_new_b_old_predecessor_history) + (cf_head_old_predecessor_history)) + ((cf_head_old_predecessor_history) + (cf_head_old_predecessor_history)))) + ((((cf_new_b_old_predecessor_history) + (cf_head_old_predecessor_history)) * S ((cf_new_b_old_predecessor_history) + (cf_head_old_predecessor_history)) + ((cf_head_old_predecessor_history) + (cf_head_old_predecessor_history))) + (((cf_new_b_old_predecessor_history) + (cf_head_old_predecessor_history)) * S ((cf_new_b_old_predecessor_history) + (cf_head_old_predecessor_history)) + ((cf_head_old_predecessor_history) + (cf_head_old_predecessor_history))))) = S ((S (S cf_index_old_predecessor_history)) * e)) /\ exists ff_q_cf_old_predecessor_history_following_state. h = ff_q_cf_old_predecessor_history_following_state * S ((S (S cf_index_old_predecessor_history)) * e) + (((cf_new_a_old_predecessor_history) + (((cf_new_b_old_predecessor_history) + (cf_head_old_predecessor_history)) * S ((cf_new_b_old_predecessor_history) + (cf_head_old_predecessor_history)) + ((cf_head_old_predecessor_history) + (cf_head_old_predecessor_history)))) * S ((cf_new_a_old_predecessor_history) + (((cf_new_b_old_predecessor_history) + (cf_head_old_predecessor_history)) * S ((cf_new_b_old_predecessor_history) + (cf_head_old_predecessor_history)) + ((cf_head_old_predecessor_history) + (cf_head_old_predecessor_history)))) + ((((cf_new_b_old_predecessor_history) + (cf_head_old_predecessor_history)) * S ((cf_new_b_old_predecessor_history) + (cf_head_old_predecessor_history)) + ((cf_head_old_predecessor_history) + (cf_head_old_predecessor_history))) + (((cf_new_b_old_predecessor_history) + (cf_head_old_predecessor_history)) * S ((cf_new_b_old_predecessor_history) + (cf_head_old_predecessor_history)) + ((cf_head_old_predecessor_history) + (cf_head_old_predecessor_history))))))) /\ (cf_new_b_old_predecessor_history = cf_old_a_old_predecessor_history /\ (cf_new_a_old_predecessor_history = cf_new_b_old_predecessor_history * cf_quotient_old_predecessor_history + cf_old_b_old_predecessor_history /\ ((exists ff_lt_cf_old_predecessor_history_remainder. ff_lt_cf_old_predecessor_history_remainder + S cf_old_b_old_predecessor_history = cf_new_b_old_predecessor_history) /\ (cf_head_old_predecessor_history = S ((cf_quotient_old_predecessor_history + cf_tail_old_predecessor_history) * S (cf_quotient_old_predecessor_history + cf_tail_old_predecessor_history) + (cf_tail_old_predecessor_history + cf_tail_old_predecessor_history))))))))))))))

Complete tactic proof in conservative notation

All 81 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

81 script commands · 31 reading checkpoints · 4 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

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

Named ingredients (1)
cf convergent old history state unique
01Fix variables and assumptionsL1–7

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 k
  7. L7
    intro ht
02Separate the logical casesL8–10

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

  1. L8
    cases ht
  2. L9
    cases ht_witness
  3. L10
    cases ht_witness_right
03Establish hsL11–13

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

  1. L11
    have hs · expand full local formula (1,924 characters)have hs : ∃ cfc_old_a_old_last_step. ∃ cfc_old_b_old_last_step. ∃ cfc_tail_old_last_step. ∃ cfc_new_a_old_last_step. ∃ cfc_new_b_old_last_step. ∃ cfc_head_old_last_step. ∃ cfc_q_old_last_step. BetaAt(h,e,k,(cfc_old_a_old_last_step + ((cfc_old_b_old_last_step + cfc_tail_old_last_step) · S (cfc_old_b_old_last_step + cfc_tail_old_last_step) + (cfc_tail_old_last_step + cfc_tail_old_last_step))) · S (cfc_old_a_old_last_step + ((cfc_old_b_old_last_step + cfc_tail_old_last_step) · S (cfc_old_b_old_last_step + cfc_tail_old_last_step) + (cfc_tail_old_last_step + cfc_tail_old_last_step))) + ((cfc_old_b_old_last_step + cfc_tail_old_last_step) · S (cfc_old_b_old_last_step + cfc_tail_old_last_step) + (cfc_tail_old_last_step + cfc_tail_old_last_step) + ((cfc_old_b_old_last_step + cfc_tail_old_last_step) · S (cfc_old_b_old_last_step + cfc_tail_old_last_step) + (cfc_tail_old_last_step + cfc_tail_old_last_step)))) ∧ (BetaAt(h,e,S k,(cfc_new_a_old_last_step + ((cfc_new_b_old_last_step + cfc_head_old_last_step) · S (cfc_new_b_old_last_step + cfc_head_old_last_step) + (cfc_head_old_last_step + cfc_head_old_last_step))) · S (cfc_new_a_old_last_step + ((cfc_new_b_old_last_step + cfc_head_old_last_step) · S (cfc_new_b_old_last_step + cfc_head_old_last_step) + (cfc_head_old_last_step + cfc_head_old_last_step))) + ((cfc_new_b_old_last_step + cfc_head_old_last_step) · S (cfc_new_b_old_last_step + cfc_head_old_last_step) + (cfc_head_old_last_step + cfc_head_old_last_step) + ((cfc_new_b_old_last_step + cfc_head_old_last_step) · S (cfc_new_b_old_last_step + cfc_head_old_last_step) + (cfc_head_old_last_step + cfc_head_old_last_step)))) ∧ (cfc_new_b_old_last_step = cfc_old_a_old_last_step ∧ (cfc_new_a_old_last_step = cfc_new_b_old_last_step · cfc_q_old_last_step + cfc_old_b_old_last_step ∧ (Lt(cfc_old_b_old_last_step,cfc_new_b_old_last_step) ∧ ListCell(cfc_head_old_last_step,cfc_q_old_last_step,cfc_tail_old_last_step)))))
    Definitions: BetaAt(h,e,k,(cfc_old_a_old_last_step + ((cfc_old_b_old_last_step + cfc_tail_old_last_step) · S (cfc_old_b_old_last_step + cfc_tail_old_last_step) + (cfc_tail_old_last_step + cfc_tail_old_last_step))) · S (cfc_old_a_old_last_step + ((cfc_old_b_old_last_step + cfc_tail_old_last_step) · S (cfc_old_b_old_last_step + cfc_tail_old_last_step) + (cfc_tail_old_last_step + cfc_tail_old_last_step))) + ((cfc_old_b_old_last_step + cfc_tail_old_last_step) · S (cfc_old_b_old_last_step + cfc_tail_old_last_step) + (cfc_tail_old_last_step + cfc_tail_old_last_step) + ((cfc_old_b_old_last_step + cfc_tail_old_last_step) · S (cfc_old_b_old_last_step + cfc_tail_old_last_step) + (cfc_tail_old_last_step + cfc_tail_old_last_step))))BetaAt(h,e,S k,(cfc_new_a_old_last_step + ((cfc_new_b_old_last_step + cfc_head_old_last_step) · S (cfc_new_b_old_last_step + cfc_head_old_last_step) + (cfc_head_old_last_step + cfc_head_old_last_step))) · S (cfc_new_a_old_last_step + ((cfc_new_b_old_last_step + cfc_head_old_last_step) · S (cfc_new_b_old_last_step + cfc_head_old_last_step) + (cfc_head_old_last_step + cfc_head_old_last_step))) + ((cfc_new_b_old_last_step + cfc_head_old_last_step) · S (cfc_new_b_old_last_step + cfc_head_old_last_step) + (cfc_head_old_last_step + cfc_head_old_last_step) + ((cfc_new_b_old_last_step + cfc_head_old_last_step) · S (cfc_new_b_old_last_step + cfc_head_old_last_step) + (cfc_head_old_last_step + cfc_head_old_last_step))))Lt(cfc_old_b_old_last_step,cfc_new_b_old_last_step)ListCell(cfc_head_old_last_step,cfc_q_old_last_step,cfc_tail_old_last_step)Original native command in the exact edition
  2. L12
    specialize ht_witness_right_right (k)
  3. L13
    apply ht_witness_right_right
04Construct an explicit witnessL14–14

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

  1. L14
    exists 0
05Use earlier factsL15–15

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

  1. L15
    apply zero_add
06Separate the logical casesL16–25

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

  1. L16
    cases hs
  2. L17
    cases hs_witness
  3. L18
    cases hs_witness_witness
  4. L19
    cases hs_witness_witness_witness
  5. L20
    cases hs_witness_witness_witness_witness
  6. L21
    cases hs_witness_witness_witness_witness_witness
  7. L22
    cases hs_witness_witness_witness_witness_witness_witness
  8. L23
    cases hs_witness_witness_witness_witness_witness_witness_witness
  9. L24
    cases hs_witness_witness_witness_witness_witness_witness_witness_right
  10. L25
    cases hs_witness_witness_witness_witness_witness_witness_witness_right_right
07Separate the logical casesL26–27

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

  1. L26
    cases hs_witness_witness_witness_witness_witness_witness_witness_right_right_right
  2. L27
    cases hs_witness_witness_witness_witness_witness_witness_witness_right_right_right_right
08Establish heqL28–37

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

  1. L28
    have heq : ((a = x4) /\ ((b = x5) /\ (s = x6)))
  2. L29
    specialize cf_convergent_old_history_state_unique (h)
  3. L30
    specialize cf_convergent_old_history_state_unique (e)
  4. L31
    specialize cf_convergent_old_history_state_unique (S k)
  5. L32
    specialize cf_convergent_old_history_state_unique (a)
  6. L33
    specialize cf_convergent_old_history_state_unique (b)
  7. L34
    specialize cf_convergent_old_history_state_unique (s)
  8. L35
    specialize cf_convergent_old_history_state_unique (x4)
  9. L36
    specialize cf_convergent_old_history_state_unique (x5)
  10. L37
    specialize cf_convergent_old_history_state_unique (x6)
09Use earlier factsL38–40

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

  1. L38
    apply cf_convergent_old_history_state_unique
  2. L39
    exact ht_witness_right_left
  3. L40
    exact hs_witness_witness_witness_witness_witness_witness_witness_right_left
10Separate the logical casesL41–42

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

  1. L41
    cases heq
  2. L42
    cases heq_right
11Establish hdivisorL43–46

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

  1. L43
    have hdivisor : b = x1
  2. L44
    trans x5
  3. L45
    exact heq_right_left
  4. L46
    exact hs_witness_witness_witness_witness_witness_witness_witness_right_right_left
12Establish hprefixL47–47

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

  1. L47
    have hprefix : ContinuedFractionTrace(x1,x2,x3,h,e,k)Definitions: ContinuedFractionTrace(x1,x2,x3,h,e,k)Original native command in the exact edition
13Construct an explicit witnessL48–48

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

  1. L48
    exists x
14Separate the logical casesL49–49

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

  1. L49
    split
15Use earlier factsL50–50

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

  1. L50
    exact ht_witness_left
16Separate the logical casesL51–51

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

  1. L51
    split
17Use earlier factsL52–52

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

  1. L52
    exact hs_witness_witness_witness_witness_witness_witness_witness_left
18Fix variables and assumptionsL53–54

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

  1. L53
    intro j
  2. L54
    intro hj
19Use earlier factsL55–63

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

  1. L55
    specialize ht_witness_right_right (j)
  2. L56
    apply ht_witness_right_right
  3. L57
    specialize lt_of_lt_of_le (j)
  4. L58
    specialize lt_of_lt_of_le (k)
  5. L59
    specialize lt_of_lt_of_le (S k)
  6. L60
    apply lt_of_lt_of_le
  7. L61
    exact hj
  8. L62
    specialize le_succ_self (k)
  9. L63
    apply le_succ_self
20Construct an explicit witnessL64–66

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

  1. L64
    exists x7
  2. L65
    exists x2
  3. L66
    exists x3
21Separate the logical casesL67–67

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

  1. L67
    split
22Calculate and transport equalitiesL68–69

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

  1. L68
    rewrite heq_left
  2. L69
    rewrite heq_right_left
23Use earlier factsL70–70

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

  1. L70
    exact hs_witness_witness_witness_witness_witness_witness_witness_right_right_right_left
24Separate the logical casesL71–71

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

  1. L71
    split
25Calculate and transport equalitiesL72–72

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

  1. L72
    rewrite heq_right_left
26Use earlier factsL73–73

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

  1. L73
    exact hs_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_left
27Separate the logical casesL74–74

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

  1. L74
    split
28Calculate and transport equalitiesL75–75

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

  1. L75
    rewrite heq_right_right
29Use earlier factsL76–76

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

  1. L76
    exact hs_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right
30Calculate and transport equalitiesL77–80

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

  1. L77
    rewrite hdivisor
  2. L78
    rewrite hdivisor
  3. L79
    rewrite hdivisor
  4. L80
    rewrite hdivisor
31Use earlier factsL81–81

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

  1. L81
    exact hprefix

Library-wide reading audit

Original defined command ledger · 81 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro s
  4. 0004intro h
  5. 0005intro e
  6. 0006intro k
  7. 0007intro ht
  8. 0008cases ht
  9. 0009cases ht_witness
  10. 0010cases ht_witness_right
  11. 0011have hs : ∃ cfc_old_a_old_last_step. ∃ cfc_old_b_old_last_step. ∃ cfc_tail_old_last_step. ∃ cfc_new_a_old_last_step. ∃ cfc_new_b_old_last_step. ∃ cfc_head_old_last_step. ∃ cfc_q_old_last_step. BetaAt(h,e,k,(cfc_old_a_old_last_step + ((cfc_old_b_old_last_step + cfc_tail_old_last_step) · S (cfc_old_b_old_last_step + cfc_tail_old_last_step) + (cfc_tail_old_last_step + cfc_tail_old_last_step))) · S (cfc_old_a_old_last_step + ((cfc_old_b_old_last_step + cfc_tail_old_last_step) · S (cfc_old_b_old_last_step + cfc_tail_old_last_step) + (cfc_tail_old_last_step + cfc_tail_old_last_step))) + ((cfc_old_b_old_last_step + cfc_tail_old_last_step) · S (cfc_old_b_old_last_step + cfc_tail_old_last_step) + (cfc_tail_old_last_step + cfc_tail_old_last_step) + ((cfc_old_b_old_last_step + cfc_tail_old_last_step) · S (cfc_old_b_old_last_step + cfc_tail_old_last_step) + (cfc_tail_old_last_step + cfc_tail_old_last_step)))) ∧ (BetaAt(h,e,S k,(cfc_new_a_old_last_step + ((cfc_new_b_old_last_step + cfc_head_old_last_step) · S (cfc_new_b_old_last_step + cfc_head_old_last_step) + (cfc_head_old_last_step + cfc_head_old_last_step))) · S (cfc_new_a_old_last_step + ((cfc_new_b_old_last_step + cfc_head_old_last_step) · S (cfc_new_b_old_last_step + cfc_head_old_last_step) + (cfc_head_old_last_step + cfc_head_old_last_step))) + ((cfc_new_b_old_last_step + cfc_head_old_last_step) · S (cfc_new_b_old_last_step + cfc_head_old_last_step) + (cfc_head_old_last_step + cfc_head_old_last_step) + ((cfc_new_b_old_last_step + cfc_head_old_last_step) · S (cfc_new_b_old_last_step + cfc_head_old_last_step) + (cfc_head_old_last_step + cfc_head_old_last_step)))) ∧ (cfc_new_b_old_last_step = cfc_old_a_old_last_step ∧ (cfc_new_a_old_last_step = cfc_new_b_old_last_step · cfc_q_old_last_step + cfc_old_b_old_last_step ∧ (Lt(cfc_old_b_old_last_step,cfc_new_b_old_last_step) ∧ ListCell(cfc_head_old_last_step,cfc_q_old_last_step,cfc_tail_old_last_step)))))
  12. 0012specialize ht_witness_right_right (k)
  13. 0013apply ht_witness_right_right
  14. 0014exists 0
  15. 0015apply zero_add
  16. 0016cases hs
  17. 0017cases hs_witness
  18. 0018cases hs_witness_witness
  19. 0019cases hs_witness_witness_witness
  20. 0020cases hs_witness_witness_witness_witness
  21. 0021cases hs_witness_witness_witness_witness_witness
  22. 0022cases hs_witness_witness_witness_witness_witness_witness
  23. 0023cases hs_witness_witness_witness_witness_witness_witness_witness
  24. 0024cases hs_witness_witness_witness_witness_witness_witness_witness_right
  25. 0025cases hs_witness_witness_witness_witness_witness_witness_witness_right_right
  26. 0026cases hs_witness_witness_witness_witness_witness_witness_witness_right_right_right
  27. 0027cases hs_witness_witness_witness_witness_witness_witness_witness_right_right_right_right
  28. 0028have heq : ((a = x4) /\ ((b = x5) /\ (s = x6)))
  29. 0029specialize cf_convergent_old_history_state_unique (h)
  30. 0030specialize cf_convergent_old_history_state_unique (e)
  31. 0031specialize cf_convergent_old_history_state_unique (S k)
  32. 0032specialize cf_convergent_old_history_state_unique (a)
  33. 0033specialize cf_convergent_old_history_state_unique (b)
  34. 0034specialize cf_convergent_old_history_state_unique (s)
  35. 0035specialize cf_convergent_old_history_state_unique (x4)
  36. 0036specialize cf_convergent_old_history_state_unique (x5)
  37. 0037specialize cf_convergent_old_history_state_unique (x6)
  38. 0038apply cf_convergent_old_history_state_unique
  39. 0039exact ht_witness_right_left
  40. 0040exact hs_witness_witness_witness_witness_witness_witness_witness_right_left
  41. 0041cases heq
  42. 0042cases heq_right
  43. 0043have hdivisor : b = x1
  44. 0044trans x5
  45. 0045exact heq_right_left
  46. 0046exact hs_witness_witness_witness_witness_witness_witness_witness_right_right_left
  47. 0047have hprefix : ContinuedFractionTrace(x1,x2,x3,h,e,k)
  48. 0048exists x
  49. 0049split
  50. 0050exact ht_witness_left
  51. 0051split
  52. 0052exact hs_witness_witness_witness_witness_witness_witness_witness_left
  53. 0053intro j
  54. 0054intro hj
  55. 0055specialize ht_witness_right_right (j)
  56. 0056apply ht_witness_right_right
  57. 0057specialize lt_of_lt_of_le (j)
  58. 0058specialize lt_of_lt_of_le (k)
  59. 0059specialize lt_of_lt_of_le (S k)
  60. 0060apply lt_of_lt_of_le
  61. 0061exact hj
  62. 0062specialize le_succ_self (k)
  63. 0063apply le_succ_self
  64. 0064exists x7
  65. 0065exists x2
  66. 0066exists x3
  67. 0067split
  68. 0068rewrite heq_left
  69. 0069rewrite heq_right_left
  70. 0070exact hs_witness_witness_witness_witness_witness_witness_witness_right_right_right_left
  71. 0071split
  72. 0072rewrite heq_right_left
  73. 0073exact hs_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_left
  74. 0074split
  75. 0075rewrite heq_right_right
  76. 0076exact hs_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right
  77. 0077rewrite hdivisor
  78. 0078rewrite hdivisor
  79. 0079rewrite hdivisor
  80. 0080rewrite hdivisor
  81. 0081exact hprefix