BA0040

cf_convergent_actual_prefix_index_bound

Every actual matrix prefix consumes at most the available number of G071 quotients; out-of-range indices cannot satisfy Convergent.

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

∀ k. ∀ a. ∀ b. ∀ s. ∀ h. ∀ e. ∀ L. ∀ H. ∀ E. ∀ u. ∀ U. ∀ v. ∀ V. ContinuedFractionTrace(a,b,s,h,e,L) → ConvergentMatrixTrace(s,H,E,k,u,U,v,V) → Le(k,L)

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

Definition DAG

ContinuedFractionTrace(a,b,s,u,v,ell) · 2ConvergentMatrixTrace(s,h,e,k,u,U,v,V) · 2Le(a,b) · 1Lt(a,b) · 1

Actual proof prerequisites

cf_convergent_euclidean_matrix_step_alignmentsucc_le_succ · checked external prerequisite
Original expanded first-order statement 
forall k a b s h e L H E u U v V. (exists cf_gcd_bound_source. ((((exists ff_h_cf_bound_source_initial_state. ff_h_cf_bound_source_initial_state + S (((cf_gcd_bound_source) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_bound_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_bound_source_initial_state. h = ff_q_cf_bound_source_initial_state * S ((S (0)) * e) + (((cf_gcd_bound_source) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_bound_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_bound_source_terminal_state. ff_h_cf_bound_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_bound_source_terminal_state. h = ff_q_cf_bound_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_bound_source. (exists ff_lt_cf_bound_source_index. ff_lt_cf_bound_source_index + S cf_index_bound_source = L) -> exists cf_old_a_bound_source cf_old_b_bound_source cf_tail_bound_source cf_new_a_bound_source cf_new_b_bound_source cf_head_bound_source cf_quotient_bound_source. ((((exists ff_h_cf_bound_source_previous_state. ff_h_cf_bound_source_previous_state + S (((cf_old_a_bound_source) + (((cf_old_b_bound_source) + (cf_tail_bound_source)) * S ((cf_old_b_bound_source) + (cf_tail_bound_source)) + ((cf_tail_bound_source) + (cf_tail_bound_source)))) * S ((cf_old_a_bound_source) + (((cf_old_b_bound_source) + (cf_tail_bound_source)) * S ((cf_old_b_bound_source) + (cf_tail_bound_source)) + ((cf_tail_bound_source) + (cf_tail_bound_source)))) + ((((cf_old_b_bound_source) + (cf_tail_bound_source)) * S ((cf_old_b_bound_source) + (cf_tail_bound_source)) + ((cf_tail_bound_source) + (cf_tail_bound_source))) + (((cf_old_b_bound_source) + (cf_tail_bound_source)) * S ((cf_old_b_bound_source) + (cf_tail_bound_source)) + ((cf_tail_bound_source) + (cf_tail_bound_source))))) = S ((S (cf_index_bound_source)) * e)) /\ exists ff_q_cf_bound_source_previous_state. h = ff_q_cf_bound_source_previous_state * S ((S (cf_index_bound_source)) * e) + (((cf_old_a_bound_source) + (((cf_old_b_bound_source) + (cf_tail_bound_source)) * S ((cf_old_b_bound_source) + (cf_tail_bound_source)) + ((cf_tail_bound_source) + (cf_tail_bound_source)))) * S ((cf_old_a_bound_source) + (((cf_old_b_bound_source) + (cf_tail_bound_source)) * S ((cf_old_b_bound_source) + (cf_tail_bound_source)) + ((cf_tail_bound_source) + (cf_tail_bound_source)))) + ((((cf_old_b_bound_source) + (cf_tail_bound_source)) * S ((cf_old_b_bound_source) + (cf_tail_bound_source)) + ((cf_tail_bound_source) + (cf_tail_bound_source))) + (((cf_old_b_bound_source) + (cf_tail_bound_source)) * S ((cf_old_b_bound_source) + (cf_tail_bound_source)) + ((cf_tail_bound_source) + (cf_tail_bound_source))))))) /\ ((((exists ff_h_cf_bound_source_following_state. ff_h_cf_bound_source_following_state + S (((cf_new_a_bound_source) + (((cf_new_b_bound_source) + (cf_head_bound_source)) * S ((cf_new_b_bound_source) + (cf_head_bound_source)) + ((cf_head_bound_source) + (cf_head_bound_source)))) * S ((cf_new_a_bound_source) + (((cf_new_b_bound_source) + (cf_head_bound_source)) * S ((cf_new_b_bound_source) + (cf_head_bound_source)) + ((cf_head_bound_source) + (cf_head_bound_source)))) + ((((cf_new_b_bound_source) + (cf_head_bound_source)) * S ((cf_new_b_bound_source) + (cf_head_bound_source)) + ((cf_head_bound_source) + (cf_head_bound_source))) + (((cf_new_b_bound_source) + (cf_head_bound_source)) * S ((cf_new_b_bound_source) + (cf_head_bound_source)) + ((cf_head_bound_source) + (cf_head_bound_source))))) = S ((S (S cf_index_bound_source)) * e)) /\ exists ff_q_cf_bound_source_following_state. h = ff_q_cf_bound_source_following_state * S ((S (S cf_index_bound_source)) * e) + (((cf_new_a_bound_source) + (((cf_new_b_bound_source) + (cf_head_bound_source)) * S ((cf_new_b_bound_source) + (cf_head_bound_source)) + ((cf_head_bound_source) + (cf_head_bound_source)))) * S ((cf_new_a_bound_source) + (((cf_new_b_bound_source) + (cf_head_bound_source)) * S ((cf_new_b_bound_source) + (cf_head_bound_source)) + ((cf_head_bound_source) + (cf_head_bound_source)))) + ((((cf_new_b_bound_source) + (cf_head_bound_source)) * S ((cf_new_b_bound_source) + (cf_head_bound_source)) + ((cf_head_bound_source) + (cf_head_bound_source))) + (((cf_new_b_bound_source) + (cf_head_bound_source)) * S ((cf_new_b_bound_source) + (cf_head_bound_source)) + ((cf_head_bound_source) + (cf_head_bound_source))))))) /\ (cf_new_b_bound_source = cf_old_a_bound_source /\ (cf_new_a_bound_source = cf_new_b_bound_source * cf_quotient_bound_source + cf_old_b_bound_source /\ ((exists ff_lt_cf_bound_source_remainder. ff_lt_cf_bound_source_remainder + S cf_old_b_bound_source = cf_new_b_bound_source) /\ (cf_head_bound_source = S ((cf_quotient_bound_source + cf_tail_bound_source) * S (cf_quotient_bound_source + cf_tail_bound_source) + (cf_tail_bound_source + cf_tail_bound_source))))))))))) -> (exists cfc_tail_bound_matrix. ((exists cfc_state_bound_matrixinitial. ((exists cfc_left_bound_matrixinitialcode cfc_right_bound_matrixinitialcode cfc_matrix_bound_matrixinitialcode. ((cfc_left_bound_matrixinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_bound_matrixinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_bound_matrixinitialcode = ((cfc_left_bound_matrixinitialcode) + (cfc_right_bound_matrixinitialcode)) * S ((cfc_left_bound_matrixinitialcode) + (cfc_right_bound_matrixinitialcode)) + ((cfc_right_bound_matrixinitialcode) + (cfc_right_bound_matrixinitialcode))) /\ ((cfc_state_bound_matrixinitial) = ((cfc_tail_bound_matrix) + (cfc_matrix_bound_matrixinitialcode)) * S ((cfc_tail_bound_matrix) + (cfc_matrix_bound_matrixinitialcode)) + ((cfc_matrix_bound_matrixinitialcode) + (cfc_matrix_bound_matrixinitialcode))))))) /\ (((exists ff_h_bound_matrixinitialentry. ff_h_bound_matrixinitialentry + S (cfc_state_bound_matrixinitial) = S ((S (0)) * E)) /\ exists ff_q_bound_matrixinitialentry. H = ff_q_bound_matrixinitialentry * S ((S (0)) * E) + (cfc_state_bound_matrixinitial))))) /\ ((exists cfc_state_bound_matrixterminal. ((exists cfc_left_bound_matrixterminalcode cfc_right_bound_matrixterminalcode cfc_matrix_bound_matrixterminalcode. ((cfc_left_bound_matrixterminalcode = ((u) + (U)) * S ((u) + (U)) + ((U) + (U))) /\ ((cfc_right_bound_matrixterminalcode = ((v) + (V)) * S ((v) + (V)) + ((V) + (V))) /\ ((cfc_matrix_bound_matrixterminalcode = ((cfc_left_bound_matrixterminalcode) + (cfc_right_bound_matrixterminalcode)) * S ((cfc_left_bound_matrixterminalcode) + (cfc_right_bound_matrixterminalcode)) + ((cfc_right_bound_matrixterminalcode) + (cfc_right_bound_matrixterminalcode))) /\ ((cfc_state_bound_matrixterminal) = ((s) + (cfc_matrix_bound_matrixterminalcode)) * S ((s) + (cfc_matrix_bound_matrixterminalcode)) + ((cfc_matrix_bound_matrixterminalcode) + (cfc_matrix_bound_matrixterminalcode))))))) /\ (((exists ff_h_bound_matrixterminalentry. ff_h_bound_matrixterminalentry + S (cfc_state_bound_matrixterminal) = S ((S (k)) * E)) /\ exists ff_q_bound_matrixterminalentry. H = ff_q_bound_matrixterminalentry * S ((S (k)) * E) + (cfc_state_bound_matrixterminal))))) /\ (forall cfc_index_bound_matrix. (exists cfba_gap_bound_matrixbound. cfba_gap_bound_matrixbound + S (cfc_index_bound_matrix) = (k)) -> exists cfc_old_bound_matrix cfc_a_bound_matrix cfc_b_bound_matrix cfc_c_bound_matrix cfc_d_bound_matrix cfc_new_bound_matrix cfc_quotient_bound_matrix. ((exists cfc_state_bound_matrixprevious. ((exists cfc_left_bound_matrixpreviouscode cfc_right_bound_matrixpreviouscode cfc_matrix_bound_matrixpreviouscode. ((cfc_left_bound_matrixpreviouscode = ((cfc_a_bound_matrix) + (cfc_b_bound_matrix)) * S ((cfc_a_bound_matrix) + (cfc_b_bound_matrix)) + ((cfc_b_bound_matrix) + (cfc_b_bound_matrix))) /\ ((cfc_right_bound_matrixpreviouscode = ((cfc_c_bound_matrix) + (cfc_d_bound_matrix)) * S ((cfc_c_bound_matrix) + (cfc_d_bound_matrix)) + ((cfc_d_bound_matrix) + (cfc_d_bound_matrix))) /\ ((cfc_matrix_bound_matrixpreviouscode = ((cfc_left_bound_matrixpreviouscode) + (cfc_right_bound_matrixpreviouscode)) * S ((cfc_left_bound_matrixpreviouscode) + (cfc_right_bound_matrixpreviouscode)) + ((cfc_right_bound_matrixpreviouscode) + (cfc_right_bound_matrixpreviouscode))) /\ ((cfc_state_bound_matrixprevious) = ((cfc_old_bound_matrix) + (cfc_matrix_bound_matrixpreviouscode)) * S ((cfc_old_bound_matrix) + (cfc_matrix_bound_matrixpreviouscode)) + ((cfc_matrix_bound_matrixpreviouscode) + (cfc_matrix_bound_matrixpreviouscode))))))) /\ (((exists ff_h_bound_matrixpreviousentry. ff_h_bound_matrixpreviousentry + S (cfc_state_bound_matrixprevious) = S ((S (cfc_index_bound_matrix)) * E)) /\ exists ff_q_bound_matrixpreviousentry. H = ff_q_bound_matrixpreviousentry * S ((S (cfc_index_bound_matrix)) * E) + (cfc_state_bound_matrixprevious))))) /\ ((exists cfc_state_bound_matrixfollowing. ((exists cfc_left_bound_matrixfollowingcode cfc_right_bound_matrixfollowingcode cfc_matrix_bound_matrixfollowingcode. ((cfc_left_bound_matrixfollowingcode = (((cfc_quotient_bound_matrix * cfc_a_bound_matrix + cfc_c_bound_matrix)) + ((cfc_quotient_bound_matrix * cfc_b_bound_matrix + cfc_d_bound_matrix))) * S (((cfc_quotient_bound_matrix * cfc_a_bound_matrix + cfc_c_bound_matrix)) + ((cfc_quotient_bound_matrix * cfc_b_bound_matrix + cfc_d_bound_matrix))) + (((cfc_quotient_bound_matrix * cfc_b_bound_matrix + cfc_d_bound_matrix)) + ((cfc_quotient_bound_matrix * cfc_b_bound_matrix + cfc_d_bound_matrix)))) /\ ((cfc_right_bound_matrixfollowingcode = ((cfc_a_bound_matrix) + (cfc_b_bound_matrix)) * S ((cfc_a_bound_matrix) + (cfc_b_bound_matrix)) + ((cfc_b_bound_matrix) + (cfc_b_bound_matrix))) /\ ((cfc_matrix_bound_matrixfollowingcode = ((cfc_left_bound_matrixfollowingcode) + (cfc_right_bound_matrixfollowingcode)) * S ((cfc_left_bound_matrixfollowingcode) + (cfc_right_bound_matrixfollowingcode)) + ((cfc_right_bound_matrixfollowingcode) + (cfc_right_bound_matrixfollowingcode))) /\ ((cfc_state_bound_matrixfollowing) = ((cfc_new_bound_matrix) + (cfc_matrix_bound_matrixfollowingcode)) * S ((cfc_new_bound_matrix) + (cfc_matrix_bound_matrixfollowingcode)) + ((cfc_matrix_bound_matrixfollowingcode) + (cfc_matrix_bound_matrixfollowingcode))))))) /\ (((exists ff_h_bound_matrixfollowingentry. ff_h_bound_matrixfollowingentry + S (cfc_state_bound_matrixfollowing) = S ((S (S cfc_index_bound_matrix)) * E)) /\ exists ff_q_bound_matrixfollowingentry. H = ff_q_bound_matrixfollowingentry * S ((S (S cfc_index_bound_matrix)) * E) + (cfc_state_bound_matrixfollowing))))) /\ (cfc_new_bound_matrix = S ((cfc_quotient_bound_matrix + cfc_old_bound_matrix) * S (cfc_quotient_bound_matrix + cfc_old_bound_matrix) + (cfc_old_bound_matrix + cfc_old_bound_matrix))))))))) -> (exists cfba_bound_bound_result. cfba_bound_bound_result + (k) = (L))

Complete tactic proof in conservative notation

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

83 script commands · 13 reading checkpoints · 1 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 euclidean matrix step alignment
01Induction on kL1–10

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

  1. L1
    induction k
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro s
  5. L5
    intro h
  6. L6
    intro e
  7. L7
    intro L
  8. L8
    intro H
  9. L9
    intro E
  10. L10
    intro u
02Fix variables and assumptionsL11–15

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

  1. L11
    intro U
  2. L12
    intro v
  3. L13
    intro V
  4. L14
    intro hold
  5. L15
    intro hnew
03Construct an explicit witnessL16–16

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

  1. L16
    exists L
04Calculate and transport equalitiesL17–17

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

  1. L17
    simp
05Fix variables and assumptionsL18–27

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

  1. L18
    intro a
  2. L19
    intro b
  3. L20
    intro s
  4. L21
    intro h
  5. L22
    intro e
  6. L23
    intro L
  7. L24
    intro H
  8. L25
    intro E
  9. L26
    intro u
  10. L27
    intro U
06Fix variables and assumptionsL28–31

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

  1. L28
    intro v
  2. L29
    intro V
  3. L30
    intro hold
  4. L31
    intro hnew
07Establish haL32–41

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

  1. L32
    have ha · expand full local formula (752 characters)have ha : ∃ cfc_r_bound_aligned. ∃ cfc_tail_bound_aligned. ∃ cfc_length_bound_aligned. ∃ cfc_q_bound_aligned. ∃ cfc_p_bound_aligned. ∃ cfc_P_bound_aligned. ∃ cfc_n_bound_aligned. ∃ cfc_N_bound_aligned. L = S cfc_length_bound_aligned ∧ (a = b · cfc_q_bound_aligned + cfc_r_bound_aligned ∧ (Lt(cfc_r_bound_aligned,b) ∧ (ContinuedFractionTrace(b,cfc_r_bound_aligned,cfc_tail_bound_aligned,h,e,cfc_length_bound_aligned) ∧ (ConvergentMatrixTrace(cfc_tail_bound_aligned,H,E,k,cfc_p_bound_aligned,cfc_P_bound_aligned,cfc_n_bound_aligned,cfc_N_bound_aligned) ∧ (u = cfc_q_bound_aligned · cfc_p_bound_aligned + cfc_n_bound_aligned ∧ (U = cfc_q_bound_aligned · cfc_P_bound_aligned + cfc_N_bound_aligned ∧ (v = cfc_p_bound_aligned ∧ V = cfc_P_bound_aligned)))))))
    Definitions: Lt(cfc_r_bound_aligned,b)ContinuedFractionTrace(b,cfc_r_bound_aligned,cfc_tail_bound_aligned,h,e,cfc_length_bound_aligned)ConvergentMatrixTrace(cfc_tail_bound_aligned,H,E,k,cfc_p_bound_aligned,cfc_P_bound_aligned,cfc_n_bound_aligned,cfc_N_bound_aligned)Original native command in the exact edition
  2. L33
    specialize cf_convergent_euclidean_matrix_step_alignment (a)
  3. L34
    specialize cf_convergent_euclidean_matrix_step_alignment (b)
  4. L35
    specialize cf_convergent_euclidean_matrix_step_alignment (s)
  5. L36
    specialize cf_convergent_euclidean_matrix_step_alignment (h)
  6. L37
    specialize cf_convergent_euclidean_matrix_step_alignment (e)
  7. L38
    specialize cf_convergent_euclidean_matrix_step_alignment (L)
  8. L39
    specialize cf_convergent_euclidean_matrix_step_alignment (H)
  9. L40
    specialize cf_convergent_euclidean_matrix_step_alignment (E)
  10. L41
    specialize cf_convergent_euclidean_matrix_step_alignment (k)
08Use earlier factsL42–48

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

  1. L42
    specialize cf_convergent_euclidean_matrix_step_alignment (u)
  2. L43
    specialize cf_convergent_euclidean_matrix_step_alignment (U)
  3. L44
    specialize cf_convergent_euclidean_matrix_step_alignment (v)
  4. L45
    specialize cf_convergent_euclidean_matrix_step_alignment (V)
  5. L46
    apply cf_convergent_euclidean_matrix_step_alignment
  6. L47
    exact hold
  7. L48
    exact hnew
09Separate the logical casesL49–58

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

  1. L49
    cases ha
  2. L50
    cases ha_witness
  3. L51
    cases ha_witness_witness
  4. L52
    cases ha_witness_witness_witness
  5. L53
    cases ha_witness_witness_witness_witness
  6. L54
    cases ha_witness_witness_witness_witness_witness
  7. L55
    cases ha_witness_witness_witness_witness_witness_witness
  8. L56
    cases ha_witness_witness_witness_witness_witness_witness_witness
  9. L57
    cases ha_witness_witness_witness_witness_witness_witness_witness_witness
  10. L58
    cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right
10Separate the logical casesL59–64

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

  1. L59
    cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right
  2. L60
    cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right
  3. L61
    cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right
  4. L62
    cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right
  5. L63
    cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  6. L64
    cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right_right
11Calculate and transport equalitiesL65–65

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

  1. L65
    rewrite ha_witness_witness_witness_witness_witness_witness_witness_witness_left
12Use earlier factsL66–75

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

  1. L66
    specialize succ_le_succ (k)
  2. L67
    specialize succ_le_succ (x2)
  3. L68
    apply succ_le_succ
  4. L69
    specialize IH (b)
  5. L70
    specialize IH (x)
  6. L71
    specialize IH (x1)
  7. L72
    specialize IH (h)
  8. L73
    specialize IH (e)
  9. L74
    specialize IH (x2)
  10. L75
    specialize IH (H)
13Use earlier factsL76–83

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

  1. L76
    specialize IH (E)
  2. L77
    specialize IH (x4)
  3. L78
    specialize IH (x5)
  4. L79
    specialize IH (x6)
  5. L80
    specialize IH (x7)
  6. L81
    apply IH
  7. L82
    exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left
  8. L83
    exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_left

Library-wide reading audit

Original defined command ledger · 83 lines
  1. 0001induction k
  2. 0002intro a
  3. 0003intro b
  4. 0004intro s
  5. 0005intro h
  6. 0006intro e
  7. 0007intro L
  8. 0008intro H
  9. 0009intro E
  10. 0010intro u
  11. 0011intro U
  12. 0012intro v
  13. 0013intro V
  14. 0014intro hold
  15. 0015intro hnew
  16. 0016exists L
  17. 0017simp
  18. 0018intro a
  19. 0019intro b
  20. 0020intro s
  21. 0021intro h
  22. 0022intro e
  23. 0023intro L
  24. 0024intro H
  25. 0025intro E
  26. 0026intro u
  27. 0027intro U
  28. 0028intro v
  29. 0029intro V
  30. 0030intro hold
  31. 0031intro hnew
  32. 0032have ha : ∃ cfc_r_bound_aligned. ∃ cfc_tail_bound_aligned. ∃ cfc_length_bound_aligned. ∃ cfc_q_bound_aligned. ∃ cfc_p_bound_aligned. ∃ cfc_P_bound_aligned. ∃ cfc_n_bound_aligned. ∃ cfc_N_bound_aligned. L = S cfc_length_bound_aligned ∧ (a = b · cfc_q_bound_aligned + cfc_r_bound_aligned ∧ (Lt(cfc_r_bound_aligned,b) ∧ (ContinuedFractionTrace(b,cfc_r_bound_aligned,cfc_tail_bound_aligned,h,e,cfc_length_bound_aligned) ∧ (ConvergentMatrixTrace(cfc_tail_bound_aligned,H,E,k,cfc_p_bound_aligned,cfc_P_bound_aligned,cfc_n_bound_aligned,cfc_N_bound_aligned) ∧ (u = cfc_q_bound_aligned · cfc_p_bound_aligned + cfc_n_bound_aligned ∧ (U = cfc_q_bound_aligned · cfc_P_bound_aligned + cfc_N_bound_aligned ∧ (v = cfc_p_bound_aligned ∧ V = cfc_P_bound_aligned)))))))
  33. 0033specialize cf_convergent_euclidean_matrix_step_alignment (a)
  34. 0034specialize cf_convergent_euclidean_matrix_step_alignment (b)
  35. 0035specialize cf_convergent_euclidean_matrix_step_alignment (s)
  36. 0036specialize cf_convergent_euclidean_matrix_step_alignment (h)
  37. 0037specialize cf_convergent_euclidean_matrix_step_alignment (e)
  38. 0038specialize cf_convergent_euclidean_matrix_step_alignment (L)
  39. 0039specialize cf_convergent_euclidean_matrix_step_alignment (H)
  40. 0040specialize cf_convergent_euclidean_matrix_step_alignment (E)
  41. 0041specialize cf_convergent_euclidean_matrix_step_alignment (k)
  42. 0042specialize cf_convergent_euclidean_matrix_step_alignment (u)
  43. 0043specialize cf_convergent_euclidean_matrix_step_alignment (U)
  44. 0044specialize cf_convergent_euclidean_matrix_step_alignment (v)
  45. 0045specialize cf_convergent_euclidean_matrix_step_alignment (V)
  46. 0046apply cf_convergent_euclidean_matrix_step_alignment
  47. 0047exact hold
  48. 0048exact hnew
  49. 0049cases ha
  50. 0050cases ha_witness
  51. 0051cases ha_witness_witness
  52. 0052cases ha_witness_witness_witness
  53. 0053cases ha_witness_witness_witness_witness
  54. 0054cases ha_witness_witness_witness_witness_witness
  55. 0055cases ha_witness_witness_witness_witness_witness_witness
  56. 0056cases ha_witness_witness_witness_witness_witness_witness_witness
  57. 0057cases ha_witness_witness_witness_witness_witness_witness_witness_witness
  58. 0058cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right
  59. 0059cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right
  60. 0060cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right
  61. 0061cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right
  62. 0062cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right
  63. 0063cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  64. 0064cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right_right
  65. 0065rewrite ha_witness_witness_witness_witness_witness_witness_witness_witness_left
  66. 0066specialize succ_le_succ (k)
  67. 0067specialize succ_le_succ (x2)
  68. 0068apply succ_le_succ
  69. 0069specialize IH (b)
  70. 0070specialize IH (x)
  71. 0071specialize IH (x1)
  72. 0072specialize IH (h)
  73. 0073specialize IH (e)
  74. 0074specialize IH (x2)
  75. 0075specialize IH (H)
  76. 0076specialize IH (E)
  77. 0077specialize IH (x4)
  78. 0078specialize IH (x5)
  79. 0079specialize IH (x6)
  80. 0080specialize IH (x7)
  81. 0081apply IH
  82. 0082exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left
  83. 0083exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_left