BA003E

cf_convergent_actual_prefix_error_invariant

Ordinary HA induction on the actual nonempty quotient-prefix length derives determinant one, both alternating errors, strict decrease, and the denominator bound directly from G071 histories.

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,S k,u,U,v,V) → ConvergentErrorInvariant(a,b,u,U,v,V)

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

Definition DAG

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

Actual proof prerequisites

cf_convergent_euclidean_matrix_step_alignmentcf_convergent_matrix_empty_eliminationcf_approximation_first_recurrence_error_invariantcf_approximation_prepend_recurrence_error_invariant
Original expanded first-order statement 
forall k a b s h e L H E u U v V. (exists cf_gcd_invariant_euclidean. ((((exists ff_h_cf_invariant_euclidean_initial_state. ff_h_cf_invariant_euclidean_initial_state + S (((cf_gcd_invariant_euclidean) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_invariant_euclidean) + (((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_invariant_euclidean_initial_state. h = ff_q_cf_invariant_euclidean_initial_state * S ((S (0)) * e) + (((cf_gcd_invariant_euclidean) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_invariant_euclidean) + (((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_invariant_euclidean_terminal_state. ff_h_cf_invariant_euclidean_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_invariant_euclidean_terminal_state. h = ff_q_cf_invariant_euclidean_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_invariant_euclidean. (exists ff_lt_cf_invariant_euclidean_index. ff_lt_cf_invariant_euclidean_index + S cf_index_invariant_euclidean = L) -> exists cf_old_a_invariant_euclidean cf_old_b_invariant_euclidean cf_tail_invariant_euclidean cf_new_a_invariant_euclidean cf_new_b_invariant_euclidean cf_head_invariant_euclidean cf_quotient_invariant_euclidean. ((((exists ff_h_cf_invariant_euclidean_previous_state. ff_h_cf_invariant_euclidean_previous_state + S (((cf_old_a_invariant_euclidean) + (((cf_old_b_invariant_euclidean) + (cf_tail_invariant_euclidean)) * S ((cf_old_b_invariant_euclidean) + (cf_tail_invariant_euclidean)) + ((cf_tail_invariant_euclidean) + (cf_tail_invariant_euclidean)))) * S ((cf_old_a_invariant_euclidean) + (((cf_old_b_invariant_euclidean) + (cf_tail_invariant_euclidean)) * S ((cf_old_b_invariant_euclidean) + (cf_tail_invariant_euclidean)) + ((cf_tail_invariant_euclidean) + (cf_tail_invariant_euclidean)))) + ((((cf_old_b_invariant_euclidean) + (cf_tail_invariant_euclidean)) * S ((cf_old_b_invariant_euclidean) + (cf_tail_invariant_euclidean)) + ((cf_tail_invariant_euclidean) + (cf_tail_invariant_euclidean))) + (((cf_old_b_invariant_euclidean) + (cf_tail_invariant_euclidean)) * S ((cf_old_b_invariant_euclidean) + (cf_tail_invariant_euclidean)) + ((cf_tail_invariant_euclidean) + (cf_tail_invariant_euclidean))))) = S ((S (cf_index_invariant_euclidean)) * e)) /\ exists ff_q_cf_invariant_euclidean_previous_state. h = ff_q_cf_invariant_euclidean_previous_state * S ((S (cf_index_invariant_euclidean)) * e) + (((cf_old_a_invariant_euclidean) + (((cf_old_b_invariant_euclidean) + (cf_tail_invariant_euclidean)) * S ((cf_old_b_invariant_euclidean) + (cf_tail_invariant_euclidean)) + ((cf_tail_invariant_euclidean) + (cf_tail_invariant_euclidean)))) * S ((cf_old_a_invariant_euclidean) + (((cf_old_b_invariant_euclidean) + (cf_tail_invariant_euclidean)) * S ((cf_old_b_invariant_euclidean) + (cf_tail_invariant_euclidean)) + ((cf_tail_invariant_euclidean) + (cf_tail_invariant_euclidean)))) + ((((cf_old_b_invariant_euclidean) + (cf_tail_invariant_euclidean)) * S ((cf_old_b_invariant_euclidean) + (cf_tail_invariant_euclidean)) + ((cf_tail_invariant_euclidean) + (cf_tail_invariant_euclidean))) + (((cf_old_b_invariant_euclidean) + (cf_tail_invariant_euclidean)) * S ((cf_old_b_invariant_euclidean) + (cf_tail_invariant_euclidean)) + ((cf_tail_invariant_euclidean) + (cf_tail_invariant_euclidean))))))) /\ ((((exists ff_h_cf_invariant_euclidean_following_state. ff_h_cf_invariant_euclidean_following_state + S (((cf_new_a_invariant_euclidean) + (((cf_new_b_invariant_euclidean) + (cf_head_invariant_euclidean)) * S ((cf_new_b_invariant_euclidean) + (cf_head_invariant_euclidean)) + ((cf_head_invariant_euclidean) + (cf_head_invariant_euclidean)))) * S ((cf_new_a_invariant_euclidean) + (((cf_new_b_invariant_euclidean) + (cf_head_invariant_euclidean)) * S ((cf_new_b_invariant_euclidean) + (cf_head_invariant_euclidean)) + ((cf_head_invariant_euclidean) + (cf_head_invariant_euclidean)))) + ((((cf_new_b_invariant_euclidean) + (cf_head_invariant_euclidean)) * S ((cf_new_b_invariant_euclidean) + (cf_head_invariant_euclidean)) + ((cf_head_invariant_euclidean) + (cf_head_invariant_euclidean))) + (((cf_new_b_invariant_euclidean) + (cf_head_invariant_euclidean)) * S ((cf_new_b_invariant_euclidean) + (cf_head_invariant_euclidean)) + ((cf_head_invariant_euclidean) + (cf_head_invariant_euclidean))))) = S ((S (S cf_index_invariant_euclidean)) * e)) /\ exists ff_q_cf_invariant_euclidean_following_state. h = ff_q_cf_invariant_euclidean_following_state * S ((S (S cf_index_invariant_euclidean)) * e) + (((cf_new_a_invariant_euclidean) + (((cf_new_b_invariant_euclidean) + (cf_head_invariant_euclidean)) * S ((cf_new_b_invariant_euclidean) + (cf_head_invariant_euclidean)) + ((cf_head_invariant_euclidean) + (cf_head_invariant_euclidean)))) * S ((cf_new_a_invariant_euclidean) + (((cf_new_b_invariant_euclidean) + (cf_head_invariant_euclidean)) * S ((cf_new_b_invariant_euclidean) + (cf_head_invariant_euclidean)) + ((cf_head_invariant_euclidean) + (cf_head_invariant_euclidean)))) + ((((cf_new_b_invariant_euclidean) + (cf_head_invariant_euclidean)) * S ((cf_new_b_invariant_euclidean) + (cf_head_invariant_euclidean)) + ((cf_head_invariant_euclidean) + (cf_head_invariant_euclidean))) + (((cf_new_b_invariant_euclidean) + (cf_head_invariant_euclidean)) * S ((cf_new_b_invariant_euclidean) + (cf_head_invariant_euclidean)) + ((cf_head_invariant_euclidean) + (cf_head_invariant_euclidean))))))) /\ (cf_new_b_invariant_euclidean = cf_old_a_invariant_euclidean /\ (cf_new_a_invariant_euclidean = cf_new_b_invariant_euclidean * cf_quotient_invariant_euclidean + cf_old_b_invariant_euclidean /\ ((exists ff_lt_cf_invariant_euclidean_remainder. ff_lt_cf_invariant_euclidean_remainder + S cf_old_b_invariant_euclidean = cf_new_b_invariant_euclidean) /\ (cf_head_invariant_euclidean = S ((cf_quotient_invariant_euclidean + cf_tail_invariant_euclidean) * S (cf_quotient_invariant_euclidean + cf_tail_invariant_euclidean) + (cf_tail_invariant_euclidean + cf_tail_invariant_euclidean))))))))))) -> (exists cfc_tail_invariant_computation. ((exists cfc_state_invariant_computationinitial. ((exists cfc_left_invariant_computationinitialcode cfc_right_invariant_computationinitialcode cfc_matrix_invariant_computationinitialcode. ((cfc_left_invariant_computationinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_invariant_computationinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_invariant_computationinitialcode = ((cfc_left_invariant_computationinitialcode) + (cfc_right_invariant_computationinitialcode)) * S ((cfc_left_invariant_computationinitialcode) + (cfc_right_invariant_computationinitialcode)) + ((cfc_right_invariant_computationinitialcode) + (cfc_right_invariant_computationinitialcode))) /\ ((cfc_state_invariant_computationinitial) = ((cfc_tail_invariant_computation) + (cfc_matrix_invariant_computationinitialcode)) * S ((cfc_tail_invariant_computation) + (cfc_matrix_invariant_computationinitialcode)) + ((cfc_matrix_invariant_computationinitialcode) + (cfc_matrix_invariant_computationinitialcode))))))) /\ (((exists ff_h_invariant_computationinitialentry. ff_h_invariant_computationinitialentry + S (cfc_state_invariant_computationinitial) = S ((S (0)) * E)) /\ exists ff_q_invariant_computationinitialentry. H = ff_q_invariant_computationinitialentry * S ((S (0)) * E) + (cfc_state_invariant_computationinitial))))) /\ ((exists cfc_state_invariant_computationterminal. ((exists cfc_left_invariant_computationterminalcode cfc_right_invariant_computationterminalcode cfc_matrix_invariant_computationterminalcode. ((cfc_left_invariant_computationterminalcode = ((u) + (U)) * S ((u) + (U)) + ((U) + (U))) /\ ((cfc_right_invariant_computationterminalcode = ((v) + (V)) * S ((v) + (V)) + ((V) + (V))) /\ ((cfc_matrix_invariant_computationterminalcode = ((cfc_left_invariant_computationterminalcode) + (cfc_right_invariant_computationterminalcode)) * S ((cfc_left_invariant_computationterminalcode) + (cfc_right_invariant_computationterminalcode)) + ((cfc_right_invariant_computationterminalcode) + (cfc_right_invariant_computationterminalcode))) /\ ((cfc_state_invariant_computationterminal) = ((s) + (cfc_matrix_invariant_computationterminalcode)) * S ((s) + (cfc_matrix_invariant_computationterminalcode)) + ((cfc_matrix_invariant_computationterminalcode) + (cfc_matrix_invariant_computationterminalcode))))))) /\ (((exists ff_h_invariant_computationterminalentry. ff_h_invariant_computationterminalentry + S (cfc_state_invariant_computationterminal) = S ((S (S k)) * E)) /\ exists ff_q_invariant_computationterminalentry. H = ff_q_invariant_computationterminalentry * S ((S (S k)) * E) + (cfc_state_invariant_computationterminal))))) /\ (forall cfc_index_invariant_computation. (exists cfba_gap_invariant_computationbound. cfba_gap_invariant_computationbound + S (cfc_index_invariant_computation) = (S k)) -> exists cfc_old_invariant_computation cfc_a_invariant_computation cfc_b_invariant_computation cfc_c_invariant_computation cfc_d_invariant_computation cfc_new_invariant_computation cfc_quotient_invariant_computation. ((exists cfc_state_invariant_computationprevious. ((exists cfc_left_invariant_computationpreviouscode cfc_right_invariant_computationpreviouscode cfc_matrix_invariant_computationpreviouscode. ((cfc_left_invariant_computationpreviouscode = ((cfc_a_invariant_computation) + (cfc_b_invariant_computation)) * S ((cfc_a_invariant_computation) + (cfc_b_invariant_computation)) + ((cfc_b_invariant_computation) + (cfc_b_invariant_computation))) /\ ((cfc_right_invariant_computationpreviouscode = ((cfc_c_invariant_computation) + (cfc_d_invariant_computation)) * S ((cfc_c_invariant_computation) + (cfc_d_invariant_computation)) + ((cfc_d_invariant_computation) + (cfc_d_invariant_computation))) /\ ((cfc_matrix_invariant_computationpreviouscode = ((cfc_left_invariant_computationpreviouscode) + (cfc_right_invariant_computationpreviouscode)) * S ((cfc_left_invariant_computationpreviouscode) + (cfc_right_invariant_computationpreviouscode)) + ((cfc_right_invariant_computationpreviouscode) + (cfc_right_invariant_computationpreviouscode))) /\ ((cfc_state_invariant_computationprevious) = ((cfc_old_invariant_computation) + (cfc_matrix_invariant_computationpreviouscode)) * S ((cfc_old_invariant_computation) + (cfc_matrix_invariant_computationpreviouscode)) + ((cfc_matrix_invariant_computationpreviouscode) + (cfc_matrix_invariant_computationpreviouscode))))))) /\ (((exists ff_h_invariant_computationpreviousentry. ff_h_invariant_computationpreviousentry + S (cfc_state_invariant_computationprevious) = S ((S (cfc_index_invariant_computation)) * E)) /\ exists ff_q_invariant_computationpreviousentry. H = ff_q_invariant_computationpreviousentry * S ((S (cfc_index_invariant_computation)) * E) + (cfc_state_invariant_computationprevious))))) /\ ((exists cfc_state_invariant_computationfollowing. ((exists cfc_left_invariant_computationfollowingcode cfc_right_invariant_computationfollowingcode cfc_matrix_invariant_computationfollowingcode. ((cfc_left_invariant_computationfollowingcode = (((cfc_quotient_invariant_computation * cfc_a_invariant_computation + cfc_c_invariant_computation)) + ((cfc_quotient_invariant_computation * cfc_b_invariant_computation + cfc_d_invariant_computation))) * S (((cfc_quotient_invariant_computation * cfc_a_invariant_computation + cfc_c_invariant_computation)) + ((cfc_quotient_invariant_computation * cfc_b_invariant_computation + cfc_d_invariant_computation))) + (((cfc_quotient_invariant_computation * cfc_b_invariant_computation + cfc_d_invariant_computation)) + ((cfc_quotient_invariant_computation * cfc_b_invariant_computation + cfc_d_invariant_computation)))) /\ ((cfc_right_invariant_computationfollowingcode = ((cfc_a_invariant_computation) + (cfc_b_invariant_computation)) * S ((cfc_a_invariant_computation) + (cfc_b_invariant_computation)) + ((cfc_b_invariant_computation) + (cfc_b_invariant_computation))) /\ ((cfc_matrix_invariant_computationfollowingcode = ((cfc_left_invariant_computationfollowingcode) + (cfc_right_invariant_computationfollowingcode)) * S ((cfc_left_invariant_computationfollowingcode) + (cfc_right_invariant_computationfollowingcode)) + ((cfc_right_invariant_computationfollowingcode) + (cfc_right_invariant_computationfollowingcode))) /\ ((cfc_state_invariant_computationfollowing) = ((cfc_new_invariant_computation) + (cfc_matrix_invariant_computationfollowingcode)) * S ((cfc_new_invariant_computation) + (cfc_matrix_invariant_computationfollowingcode)) + ((cfc_matrix_invariant_computationfollowingcode) + (cfc_matrix_invariant_computationfollowingcode))))))) /\ (((exists ff_h_invariant_computationfollowingentry. ff_h_invariant_computationfollowingentry + S (cfc_state_invariant_computationfollowing) = S ((S (S cfc_index_invariant_computation)) * E)) /\ exists ff_q_invariant_computationfollowingentry. H = ff_q_invariant_computationfollowingentry * S ((S (S cfc_index_invariant_computation)) * E) + (cfc_state_invariant_computationfollowing))))) /\ (cfc_new_invariant_computation = S ((cfc_quotient_invariant_computation + cfc_old_invariant_computation) * S (cfc_quotient_invariant_computation + cfc_old_invariant_computation) + (cfc_old_invariant_computation + cfc_old_invariant_computation))))))))) -> (exists cfba_error_invariant_output cfba_previous_error_invariant_output. (((((u * V + 1 = U * v) /\ ((a * v = b * u + cfba_error_invariant_output) /\ (b * U = a * V + cfba_previous_error_invariant_output)))) \/ (((U * v + 1 = u * V) /\ ((b * u = a * v + cfba_error_invariant_output) /\ (a * V = b * U + cfba_previous_error_invariant_output))))) /\ ((exists cfba_gap_invariant_outputdecrease. cfba_gap_invariant_outputdecrease + S (cfba_error_invariant_output) = (cfba_previous_error_invariant_output)) /\ (exists cfba_bound_invariant_outputprevious_bound. cfba_bound_invariant_outputprevious_bound + (cfba_previous_error_invariant_output) = (b)))))

Complete tactic proof in conservative notation

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

165 script commands · 21 reading checkpoints · 3 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 (4)
cf convergent euclidean matrix step alignmentcf convergent matrix empty eliminationcf approximation first recurrence error invariantcf approximation prepend recurrence error invariant
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
03Establish haL16–25

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

  1. L16
    have ha · expand full local formula (864 characters)have ha : ∃ cfc_r_invariant_aligned. ∃ cfc_tail_invariant_aligned. ∃ cfc_length_invariant_aligned. ∃ cfc_q_invariant_aligned. ∃ cfc_p_invariant_aligned. ∃ cfc_P_invariant_aligned. ∃ cfc_n_invariant_aligned. ∃ cfc_N_invariant_aligned. L = S cfc_length_invariant_aligned ∧ (a = b · cfc_q_invariant_aligned + cfc_r_invariant_aligned ∧ (Lt(cfc_r_invariant_aligned,b) ∧ (ContinuedFractionTrace(b,cfc_r_invariant_aligned,cfc_tail_invariant_aligned,h,e,cfc_length_invariant_aligned) ∧ (ConvergentMatrixTrace(cfc_tail_invariant_aligned,H,E,0,cfc_p_invariant_aligned,cfc_P_invariant_aligned,cfc_n_invariant_aligned,cfc_N_invariant_aligned) ∧ (u = cfc_q_invariant_aligned · cfc_p_invariant_aligned + cfc_n_invariant_aligned ∧ (U = cfc_q_invariant_aligned · cfc_P_invariant_aligned + cfc_N_invariant_aligned ∧ (v = cfc_p_invariant_aligned ∧ V = cfc_P_invariant_aligned)))))))
    Definitions: Lt(cfc_r_invariant_aligned,b)ContinuedFractionTrace(b,cfc_r_invariant_aligned,cfc_tail_invariant_aligned,h,e,cfc_length_invariant_aligned)ConvergentMatrixTrace(cfc_tail_invariant_aligned,H,E,0,cfc_p_invariant_aligned,cfc_P_invariant_aligned,cfc_n_invariant_aligned,cfc_N_invariant_aligned)Original native command in the exact edition
  2. L17
    specialize cf_convergent_euclidean_matrix_step_alignment (a)
  3. L18
    specialize cf_convergent_euclidean_matrix_step_alignment (b)
  4. L19
    specialize cf_convergent_euclidean_matrix_step_alignment (s)
  5. L20
    specialize cf_convergent_euclidean_matrix_step_alignment (h)
  6. L21
    specialize cf_convergent_euclidean_matrix_step_alignment (e)
  7. L22
    specialize cf_convergent_euclidean_matrix_step_alignment (L)
  8. L23
    specialize cf_convergent_euclidean_matrix_step_alignment (H)
  9. L24
    specialize cf_convergent_euclidean_matrix_step_alignment (E)
  10. L25
    specialize cf_convergent_euclidean_matrix_step_alignment (0)
04Use earlier factsL26–32

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

  1. L26
    specialize cf_convergent_euclidean_matrix_step_alignment (u)
  2. L27
    specialize cf_convergent_euclidean_matrix_step_alignment (U)
  3. L28
    specialize cf_convergent_euclidean_matrix_step_alignment (v)
  4. L29
    specialize cf_convergent_euclidean_matrix_step_alignment (V)
  5. L30
    apply cf_convergent_euclidean_matrix_step_alignment
  6. L31
    exact hold
  7. L32
    exact hnew
05Separate the logical casesL33–42

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

  1. L33
    cases ha
  2. L34
    cases ha_witness
  3. L35
    cases ha_witness_witness
  4. L36
    cases ha_witness_witness_witness
  5. L37
    cases ha_witness_witness_witness_witness
  6. L38
    cases ha_witness_witness_witness_witness_witness
  7. L39
    cases ha_witness_witness_witness_witness_witness_witness
  8. L40
    cases ha_witness_witness_witness_witness_witness_witness_witness
  9. L41
    cases ha_witness_witness_witness_witness_witness_witness_witness_witness
  10. L42
    cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right
06Separate the logical casesL43–48

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

  1. L43
    cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right
  2. L44
    cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right
  3. L45
    cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right
  4. L46
    cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right
  5. L47
    cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  6. L48
    cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right_right
07Establish hzL49–58

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

  1. L49
    have hz : ((x4 = 1) /\ ((x5 = 0) /\ ((x6 = 0) /\ (x7 = 1))))
  2. L50
    specialize cf_convergent_matrix_empty_elimination (x1)
  3. L51
    specialize cf_convergent_matrix_empty_elimination (H)
  4. L52
    specialize cf_convergent_matrix_empty_elimination (E)
  5. L53
    specialize cf_convergent_matrix_empty_elimination (x4)
  6. L54
    specialize cf_convergent_matrix_empty_elimination (x5)
  7. L55
    specialize cf_convergent_matrix_empty_elimination (x6)
  8. L56
    specialize cf_convergent_matrix_empty_elimination (x7)
  9. L57
    apply cf_convergent_matrix_empty_elimination
  10. L58
    exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_left
08Separate the logical casesL59–61

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

  1. L59
    cases hz
  2. L60
    cases hz_right
  3. L61
    cases hz_right_right
09Use earlier factsL62–71

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

  1. L62
    specialize cf_approximation_first_recurrence_error_invariant (a)
  2. L63
    specialize cf_approximation_first_recurrence_error_invariant (b)
  3. L64
    specialize cf_approximation_first_recurrence_error_invariant (x3)
  4. L65
    specialize cf_approximation_first_recurrence_error_invariant (x)
  5. L66
    specialize cf_approximation_first_recurrence_error_invariant (u)
  6. L67
    specialize cf_approximation_first_recurrence_error_invariant (U)
  7. L68
    specialize cf_approximation_first_recurrence_error_invariant (v)
  8. L69
    specialize cf_approximation_first_recurrence_error_invariant (V)
  9. L70
    specialize cf_approximation_first_recurrence_error_invariant (x4)
  10. L71
    specialize cf_approximation_first_recurrence_error_invariant (x5)
10Use earlier factsL72–81

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

  1. L72
    specialize cf_approximation_first_recurrence_error_invariant (x6)
  2. L73
    specialize cf_approximation_first_recurrence_error_invariant (x7)
  3. L74
    apply cf_approximation_first_recurrence_error_invariant
  4. L75
    exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_left
  5. L76
    exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left
  6. L77
    exact hz_left
  7. L78
    exact hz_right_left
  8. L79
    exact hz_right_right_left
  9. L80
    exact hz_right_right_right
  10. L81
    exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_left
11Use earlier factsL82–84

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

  1. L82
    exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right_left
  2. L83
    exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right_right_left
  3. L84
    exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right_right_right
12Fix variables and assumptionsL85–94

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

  1. L85
    intro a
  2. L86
    intro b
  3. L87
    intro s
  4. L88
    intro h
  5. L89
    intro e
  6. L90
    intro L
  7. L91
    intro H
  8. L92
    intro E
  9. L93
    intro u
  10. L94
    intro U
13Fix variables and assumptionsL95–98

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

  1. L95
    intro v
  2. L96
    intro V
  3. L97
    intro hold
  4. L98
    intro hnew
14Establish haL99–108

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

  1. L99
    have ha · expand full local formula (866 characters)have ha : ∃ cfc_r_invariant_aligned. ∃ cfc_tail_invariant_aligned. ∃ cfc_length_invariant_aligned. ∃ cfc_q_invariant_aligned. ∃ cfc_p_invariant_aligned. ∃ cfc_P_invariant_aligned. ∃ cfc_n_invariant_aligned. ∃ cfc_N_invariant_aligned. L = S cfc_length_invariant_aligned ∧ (a = b · cfc_q_invariant_aligned + cfc_r_invariant_aligned ∧ (Lt(cfc_r_invariant_aligned,b) ∧ (ContinuedFractionTrace(b,cfc_r_invariant_aligned,cfc_tail_invariant_aligned,h,e,cfc_length_invariant_aligned) ∧ (ConvergentMatrixTrace(cfc_tail_invariant_aligned,H,E,S k,cfc_p_invariant_aligned,cfc_P_invariant_aligned,cfc_n_invariant_aligned,cfc_N_invariant_aligned) ∧ (u = cfc_q_invariant_aligned · cfc_p_invariant_aligned + cfc_n_invariant_aligned ∧ (U = cfc_q_invariant_aligned · cfc_P_invariant_aligned + cfc_N_invariant_aligned ∧ (v = cfc_p_invariant_aligned ∧ V = cfc_P_invariant_aligned)))))))
    Definitions: Lt(cfc_r_invariant_aligned,b)ContinuedFractionTrace(b,cfc_r_invariant_aligned,cfc_tail_invariant_aligned,h,e,cfc_length_invariant_aligned)ConvergentMatrixTrace(cfc_tail_invariant_aligned,H,E,S k,cfc_p_invariant_aligned,cfc_P_invariant_aligned,cfc_n_invariant_aligned,cfc_N_invariant_aligned)Original native command in the exact edition
  2. L100
    specialize cf_convergent_euclidean_matrix_step_alignment (a)
  3. L101
    specialize cf_convergent_euclidean_matrix_step_alignment (b)
  4. L102
    specialize cf_convergent_euclidean_matrix_step_alignment (s)
  5. L103
    specialize cf_convergent_euclidean_matrix_step_alignment (h)
  6. L104
    specialize cf_convergent_euclidean_matrix_step_alignment (e)
  7. L105
    specialize cf_convergent_euclidean_matrix_step_alignment (L)
  8. L106
    specialize cf_convergent_euclidean_matrix_step_alignment (H)
  9. L107
    specialize cf_convergent_euclidean_matrix_step_alignment (E)
  10. L108
    specialize cf_convergent_euclidean_matrix_step_alignment (S k)
15Use earlier factsL109–115

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

  1. L109
    specialize cf_convergent_euclidean_matrix_step_alignment (u)
  2. L110
    specialize cf_convergent_euclidean_matrix_step_alignment (U)
  3. L111
    specialize cf_convergent_euclidean_matrix_step_alignment (v)
  4. L112
    specialize cf_convergent_euclidean_matrix_step_alignment (V)
  5. L113
    apply cf_convergent_euclidean_matrix_step_alignment
  6. L114
    exact hold
  7. L115
    exact hnew
16Separate the logical casesL116–125

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

  1. L116
    cases ha
  2. L117
    cases ha_witness
  3. L118
    cases ha_witness_witness
  4. L119
    cases ha_witness_witness_witness
  5. L120
    cases ha_witness_witness_witness_witness
  6. L121
    cases ha_witness_witness_witness_witness_witness
  7. L122
    cases ha_witness_witness_witness_witness_witness_witness
  8. L123
    cases ha_witness_witness_witness_witness_witness_witness_witness
  9. L124
    cases ha_witness_witness_witness_witness_witness_witness_witness_witness
  10. L125
    cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right
17Separate the logical casesL126–131

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

  1. L126
    cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right
  2. L127
    cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right
  3. L128
    cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right
  4. L129
    cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right
  5. L130
    cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  6. L131
    cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right_right
18Use earlier factsL132–141

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

  1. L132
    specialize cf_approximation_prepend_recurrence_error_invariant (a)
  2. L133
    specialize cf_approximation_prepend_recurrence_error_invariant (b)
  3. L134
    specialize cf_approximation_prepend_recurrence_error_invariant (x3)
  4. L135
    specialize cf_approximation_prepend_recurrence_error_invariant (x)
  5. L136
    specialize cf_approximation_prepend_recurrence_error_invariant (u)
  6. L137
    specialize cf_approximation_prepend_recurrence_error_invariant (U)
  7. L138
    specialize cf_approximation_prepend_recurrence_error_invariant (v)
  8. L139
    specialize cf_approximation_prepend_recurrence_error_invariant (V)
  9. L140
    specialize cf_approximation_prepend_recurrence_error_invariant (x4)
  10. L141
    specialize cf_approximation_prepend_recurrence_error_invariant (x5)
19Use earlier factsL142–151

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

  1. L142
    specialize cf_approximation_prepend_recurrence_error_invariant (x6)
  2. L143
    specialize cf_approximation_prepend_recurrence_error_invariant (x7)
  3. L144
    apply cf_approximation_prepend_recurrence_error_invariant
  4. L145
    exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_left
  5. L146
    exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left
  6. L147
    exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_left
  7. L148
    exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right_left
  8. L149
    exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right_right_left
  9. L150
    exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right_right_right
  10. L151
    specialize IH (b)
20Use earlier factsL152–161

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

  1. L152
    specialize IH (x)
  2. L153
    specialize IH (x1)
  3. L154
    specialize IH (h)
  4. L155
    specialize IH (e)
  5. L156
    specialize IH (x2)
  6. L157
    specialize IH (H)
  7. L158
    specialize IH (E)
  8. L159
    specialize IH (x4)
  9. L160
    specialize IH (x5)
  10. L161
    specialize IH (x6)
21Use earlier factsL162–165

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

  1. L162
    specialize IH (x7)
  2. L163
    apply IH
  3. L164
    exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left
  4. L165
    exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_left

Library-wide reading audit

Original defined command ledger · 165 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. 0016have ha : ∃ cfc_r_invariant_aligned. ∃ cfc_tail_invariant_aligned. ∃ cfc_length_invariant_aligned. ∃ cfc_q_invariant_aligned. ∃ cfc_p_invariant_aligned. ∃ cfc_P_invariant_aligned. ∃ cfc_n_invariant_aligned. ∃ cfc_N_invariant_aligned. L = S cfc_length_invariant_aligned ∧ (a = b · cfc_q_invariant_aligned + cfc_r_invariant_aligned ∧ (Lt(cfc_r_invariant_aligned,b) ∧ (ContinuedFractionTrace(b,cfc_r_invariant_aligned,cfc_tail_invariant_aligned,h,e,cfc_length_invariant_aligned) ∧ (ConvergentMatrixTrace(cfc_tail_invariant_aligned,H,E,0,cfc_p_invariant_aligned,cfc_P_invariant_aligned,cfc_n_invariant_aligned,cfc_N_invariant_aligned) ∧ (u = cfc_q_invariant_aligned · cfc_p_invariant_aligned + cfc_n_invariant_aligned ∧ (U = cfc_q_invariant_aligned · cfc_P_invariant_aligned + cfc_N_invariant_aligned ∧ (v = cfc_p_invariant_aligned ∧ V = cfc_P_invariant_aligned)))))))
  17. 0017specialize cf_convergent_euclidean_matrix_step_alignment (a)
  18. 0018specialize cf_convergent_euclidean_matrix_step_alignment (b)
  19. 0019specialize cf_convergent_euclidean_matrix_step_alignment (s)
  20. 0020specialize cf_convergent_euclidean_matrix_step_alignment (h)
  21. 0021specialize cf_convergent_euclidean_matrix_step_alignment (e)
  22. 0022specialize cf_convergent_euclidean_matrix_step_alignment (L)
  23. 0023specialize cf_convergent_euclidean_matrix_step_alignment (H)
  24. 0024specialize cf_convergent_euclidean_matrix_step_alignment (E)
  25. 0025specialize cf_convergent_euclidean_matrix_step_alignment (0)
  26. 0026specialize cf_convergent_euclidean_matrix_step_alignment (u)
  27. 0027specialize cf_convergent_euclidean_matrix_step_alignment (U)
  28. 0028specialize cf_convergent_euclidean_matrix_step_alignment (v)
  29. 0029specialize cf_convergent_euclidean_matrix_step_alignment (V)
  30. 0030apply cf_convergent_euclidean_matrix_step_alignment
  31. 0031exact hold
  32. 0032exact hnew
  33. 0033cases ha
  34. 0034cases ha_witness
  35. 0035cases ha_witness_witness
  36. 0036cases ha_witness_witness_witness
  37. 0037cases ha_witness_witness_witness_witness
  38. 0038cases ha_witness_witness_witness_witness_witness
  39. 0039cases ha_witness_witness_witness_witness_witness_witness
  40. 0040cases ha_witness_witness_witness_witness_witness_witness_witness
  41. 0041cases ha_witness_witness_witness_witness_witness_witness_witness_witness
  42. 0042cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right
  43. 0043cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right
  44. 0044cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right
  45. 0045cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right
  46. 0046cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right
  47. 0047cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  48. 0048cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right_right
  49. 0049have hz : ((x4 = 1) /\ ((x5 = 0) /\ ((x6 = 0) /\ (x7 = 1))))
  50. 0050specialize cf_convergent_matrix_empty_elimination (x1)
  51. 0051specialize cf_convergent_matrix_empty_elimination (H)
  52. 0052specialize cf_convergent_matrix_empty_elimination (E)
  53. 0053specialize cf_convergent_matrix_empty_elimination (x4)
  54. 0054specialize cf_convergent_matrix_empty_elimination (x5)
  55. 0055specialize cf_convergent_matrix_empty_elimination (x6)
  56. 0056specialize cf_convergent_matrix_empty_elimination (x7)
  57. 0057apply cf_convergent_matrix_empty_elimination
  58. 0058exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_left
  59. 0059cases hz
  60. 0060cases hz_right
  61. 0061cases hz_right_right
  62. 0062specialize cf_approximation_first_recurrence_error_invariant (a)
  63. 0063specialize cf_approximation_first_recurrence_error_invariant (b)
  64. 0064specialize cf_approximation_first_recurrence_error_invariant (x3)
  65. 0065specialize cf_approximation_first_recurrence_error_invariant (x)
  66. 0066specialize cf_approximation_first_recurrence_error_invariant (u)
  67. 0067specialize cf_approximation_first_recurrence_error_invariant (U)
  68. 0068specialize cf_approximation_first_recurrence_error_invariant (v)
  69. 0069specialize cf_approximation_first_recurrence_error_invariant (V)
  70. 0070specialize cf_approximation_first_recurrence_error_invariant (x4)
  71. 0071specialize cf_approximation_first_recurrence_error_invariant (x5)
  72. 0072specialize cf_approximation_first_recurrence_error_invariant (x6)
  73. 0073specialize cf_approximation_first_recurrence_error_invariant (x7)
  74. 0074apply cf_approximation_first_recurrence_error_invariant
  75. 0075exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_left
  76. 0076exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left
  77. 0077exact hz_left
  78. 0078exact hz_right_left
  79. 0079exact hz_right_right_left
  80. 0080exact hz_right_right_right
  81. 0081exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_left
  82. 0082exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right_left
  83. 0083exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right_right_left
  84. 0084exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right_right_right
  85. 0085intro a
  86. 0086intro b
  87. 0087intro s
  88. 0088intro h
  89. 0089intro e
  90. 0090intro L
  91. 0091intro H
  92. 0092intro E
  93. 0093intro u
  94. 0094intro U
  95. 0095intro v
  96. 0096intro V
  97. 0097intro hold
  98. 0098intro hnew
  99. 0099have ha : ∃ cfc_r_invariant_aligned. ∃ cfc_tail_invariant_aligned. ∃ cfc_length_invariant_aligned. ∃ cfc_q_invariant_aligned. ∃ cfc_p_invariant_aligned. ∃ cfc_P_invariant_aligned. ∃ cfc_n_invariant_aligned. ∃ cfc_N_invariant_aligned. L = S cfc_length_invariant_aligned ∧ (a = b · cfc_q_invariant_aligned + cfc_r_invariant_aligned ∧ (Lt(cfc_r_invariant_aligned,b) ∧ (ContinuedFractionTrace(b,cfc_r_invariant_aligned,cfc_tail_invariant_aligned,h,e,cfc_length_invariant_aligned) ∧ (ConvergentMatrixTrace(cfc_tail_invariant_aligned,H,E,S k,cfc_p_invariant_aligned,cfc_P_invariant_aligned,cfc_n_invariant_aligned,cfc_N_invariant_aligned) ∧ (u = cfc_q_invariant_aligned · cfc_p_invariant_aligned + cfc_n_invariant_aligned ∧ (U = cfc_q_invariant_aligned · cfc_P_invariant_aligned + cfc_N_invariant_aligned ∧ (v = cfc_p_invariant_aligned ∧ V = cfc_P_invariant_aligned)))))))
  100. 0100specialize cf_convergent_euclidean_matrix_step_alignment (a)
  101. 0101specialize cf_convergent_euclidean_matrix_step_alignment (b)
  102. 0102specialize cf_convergent_euclidean_matrix_step_alignment (s)
  103. 0103specialize cf_convergent_euclidean_matrix_step_alignment (h)
  104. 0104specialize cf_convergent_euclidean_matrix_step_alignment (e)
  105. 0105specialize cf_convergent_euclidean_matrix_step_alignment (L)
  106. 0106specialize cf_convergent_euclidean_matrix_step_alignment (H)
  107. 0107specialize cf_convergent_euclidean_matrix_step_alignment (E)
  108. 0108specialize cf_convergent_euclidean_matrix_step_alignment (S k)
  109. 0109specialize cf_convergent_euclidean_matrix_step_alignment (u)
  110. 0110specialize cf_convergent_euclidean_matrix_step_alignment (U)
  111. 0111specialize cf_convergent_euclidean_matrix_step_alignment (v)
  112. 0112specialize cf_convergent_euclidean_matrix_step_alignment (V)
  113. 0113apply cf_convergent_euclidean_matrix_step_alignment
  114. 0114exact hold
  115. 0115exact hnew
  116. 0116cases ha
  117. 0117cases ha_witness
  118. 0118cases ha_witness_witness
  119. 0119cases ha_witness_witness_witness
  120. 0120cases ha_witness_witness_witness_witness
  121. 0121cases ha_witness_witness_witness_witness_witness
  122. 0122cases ha_witness_witness_witness_witness_witness_witness
  123. 0123cases ha_witness_witness_witness_witness_witness_witness_witness
  124. 0124cases ha_witness_witness_witness_witness_witness_witness_witness_witness
  125. 0125cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right
  126. 0126cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right
  127. 0127cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right
  128. 0128cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right
  129. 0129cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right
  130. 0130cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  131. 0131cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right_right
  132. 0132specialize cf_approximation_prepend_recurrence_error_invariant (a)
  133. 0133specialize cf_approximation_prepend_recurrence_error_invariant (b)
  134. 0134specialize cf_approximation_prepend_recurrence_error_invariant (x3)
  135. 0135specialize cf_approximation_prepend_recurrence_error_invariant (x)
  136. 0136specialize cf_approximation_prepend_recurrence_error_invariant (u)
  137. 0137specialize cf_approximation_prepend_recurrence_error_invariant (U)
  138. 0138specialize cf_approximation_prepend_recurrence_error_invariant (v)
  139. 0139specialize cf_approximation_prepend_recurrence_error_invariant (V)
  140. 0140specialize cf_approximation_prepend_recurrence_error_invariant (x4)
  141. 0141specialize cf_approximation_prepend_recurrence_error_invariant (x5)
  142. 0142specialize cf_approximation_prepend_recurrence_error_invariant (x6)
  143. 0143specialize cf_approximation_prepend_recurrence_error_invariant (x7)
  144. 0144apply cf_approximation_prepend_recurrence_error_invariant
  145. 0145exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_left
  146. 0146exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left
  147. 0147exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_left
  148. 0148exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right_left
  149. 0149exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right_right_left
  150. 0150exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right_right_right
  151. 0151specialize IH (b)
  152. 0152specialize IH (x)
  153. 0153specialize IH (x1)
  154. 0154specialize IH (h)
  155. 0155specialize IH (e)
  156. 0156specialize IH (x2)
  157. 0157specialize IH (H)
  158. 0158specialize IH (E)
  159. 0159specialize IH (x4)
  160. 0160specialize IH (x5)
  161. 0161specialize IH (x6)
  162. 0162specialize IH (x7)
  163. 0163apply IH
  164. 0164exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left
  165. 0165exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_left