BA0040

cf_convergent_actual_prefix_index_bound

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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

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.

Exact expanded first-order arithmetic 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))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 2 declared prerequisites and contains 83 exact native proof lines.

Alpha v34 checked-use · first admitted v29 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

BA003D cf_convergent_euclidean_matrix_step_alignment succ_le_succ Stable theorem; checked-use authorized

Direct dependents

BA0042 continued_fraction_convergent_index_is_valid

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

Named ingredients (1)
cf convergent euclidean matrix step alignment

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Induction on 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: ContinuedFractionTraceConvergentMatrixTraceLt
  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 exact 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 : exists 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) /\ ((exists cfba_gap_bound_alignedbound. cfba_gap_bound_alignedbound + S (cfc_r_bound_aligned) = (b)) /\ ((exists cf_gcd_bound_alignedeuclidean. ((((exists ff_h_cf_bound_alignedeuclidean_initial_state. ff_h_cf_bound_alignedeuclidean_initial_state + S (((cf_gcd_bound_alignedeuclidean) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_bound_alignedeuclidean) + (((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_alignedeuclidean_initial_state. h = ff_q_cf_bound_alignedeuclidean_initial_state * S ((S (0)) * e) + (((cf_gcd_bound_alignedeuclidean) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_bound_alignedeuclidean) + (((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_alignedeuclidean_terminal_state. ff_h_cf_bound_alignedeuclidean_terminal_state + S (((b) + (((cfc_r_bound_aligned) + (cfc_tail_bound_aligned)) * S ((cfc_r_bound_aligned) + (cfc_tail_bound_aligned)) + ((cfc_tail_bound_aligned) + (cfc_tail_bound_aligned)))) * S ((b) + (((cfc_r_bound_aligned) + (cfc_tail_bound_aligned)) * S ((cfc_r_bound_aligned) + (cfc_tail_bound_aligned)) + ((cfc_tail_bound_aligned) + (cfc_tail_bound_aligned)))) + ((((cfc_r_bound_aligned) + (cfc_tail_bound_aligned)) * S ((cfc_r_bound_aligned) + (cfc_tail_bound_aligned)) + ((cfc_tail_bound_aligned) + (cfc_tail_bound_aligned))) + (((cfc_r_bound_aligned) + (cfc_tail_bound_aligned)) * S ((cfc_r_bound_aligned) + (cfc_tail_bound_aligned)) + ((cfc_tail_bound_aligned) + (cfc_tail_bound_aligned))))) = S ((S (cfc_length_bound_aligned)) * e)) /\ exists ff_q_cf_bound_alignedeuclidean_terminal_state. h = ff_q_cf_bound_alignedeuclidean_terminal_state * S ((S (cfc_length_bound_aligned)) * e) + (((b) + (((cfc_r_bound_aligned) + (cfc_tail_bound_aligned)) * S ((cfc_r_bound_aligned) + (cfc_tail_bound_aligned)) + ((cfc_tail_bound_aligned) + (cfc_tail_bound_aligned)))) * S ((b) + (((cfc_r_bound_aligned) + (cfc_tail_bound_aligned)) * S ((cfc_r_bound_aligned) + (cfc_tail_bound_aligned)) + ((cfc_tail_bound_aligned) + (cfc_tail_bound_aligned)))) + ((((cfc_r_bound_aligned) + (cfc_tail_bound_aligned)) * S ((cfc_r_bound_aligned) + (cfc_tail_bound_aligned)) + ((cfc_tail_bound_aligned) + (cfc_tail_bound_aligned))) + (((cfc_r_bound_aligned) + (cfc_tail_bound_aligned)) * S ((cfc_r_bound_aligned) + (cfc_tail_bound_aligned)) + ((cfc_tail_bound_aligned) + (cfc_tail_bound_aligned))))))) /\ forall cf_index_bound_alignedeuclidean. (exists ff_lt_cf_bound_alignedeuclidean_index. ff_lt_cf_bound_alignedeuclidean_index + S cf_index_bound_alignedeuclidean = cfc_length_bound_aligned) -> exists cf_old_a_bound_alignedeuclidean cf_old_b_bound_alignedeuclidean cf_tail_bound_alignedeuclidean cf_new_a_bound_alignedeuclidean cf_new_b_bound_alignedeuclidean cf_head_bound_alignedeuclidean cf_quotient_bound_alignedeuclidean. ((((exists ff_h_cf_bound_alignedeuclidean_previous_state. ff_h_cf_bound_alignedeuclidean_previous_state + S (((cf_old_a_bound_alignedeuclidean) + (((cf_old_b_bound_alignedeuclidean) + (cf_tail_bound_alignedeuclidean)) * S ((cf_old_b_bound_alignedeuclidean) + (cf_tail_bound_alignedeuclidean)) + ((cf_tail_bound_alignedeuclidean) + (cf_tail_bound_alignedeuclidean)))) * S ((cf_old_a_bound_alignedeuclidean) + (((cf_old_b_bound_alignedeuclidean) + (cf_tail_bound_alignedeuclidean)) * S ((cf_old_b_bound_alignedeuclidean) + (cf_tail_bound_alignedeuclidean)) + ((cf_tail_bound_alignedeuclidean) + (cf_tail_bound_alignedeuclidean)))) + ((((cf_old_b_bound_alignedeuclidean) + (cf_tail_bound_alignedeuclidean)) * S ((cf_old_b_bound_alignedeuclidean) + (cf_tail_bound_alignedeuclidean)) + ((cf_tail_bound_alignedeuclidean) + (cf_tail_bound_alignedeuclidean))) + (((cf_old_b_bound_alignedeuclidean) + (cf_tail_bound_alignedeuclidean)) * S ((cf_old_b_bound_alignedeuclidean) + (cf_tail_bound_alignedeuclidean)) + ((cf_tail_bound_alignedeuclidean) + (cf_tail_bound_alignedeuclidean))))) = S ((S (cf_index_bound_alignedeuclidean)) * e)) /\ exists ff_q_cf_bound_alignedeuclidean_previous_state. h = ff_q_cf_bound_alignedeuclidean_previous_state * S ((S (cf_index_bound_alignedeuclidean)) * e) + (((cf_old_a_bound_alignedeuclidean) + (((cf_old_b_bound_alignedeuclidean) + (cf_tail_bound_alignedeuclidean)) * S ((cf_old_b_bound_alignedeuclidean) + (cf_tail_bound_alignedeuclidean)) + ((cf_tail_bound_alignedeuclidean) + (cf_tail_bound_alignedeuclidean)))) * S ((cf_old_a_bound_alignedeuclidean) + (((cf_old_b_bound_alignedeuclidean) + (cf_tail_bound_alignedeuclidean)) * S ((cf_old_b_bound_alignedeuclidean) + (cf_tail_bound_alignedeuclidean)) + ((cf_tail_bound_alignedeuclidean) + (cf_tail_bound_alignedeuclidean)))) + ((((cf_old_b_bound_alignedeuclidean) + (cf_tail_bound_alignedeuclidean)) * S ((cf_old_b_bound_alignedeuclidean) + (cf_tail_bound_alignedeuclidean)) + ((cf_tail_bound_alignedeuclidean) + (cf_tail_bound_alignedeuclidean))) + (((cf_old_b_bound_alignedeuclidean) + (cf_tail_bound_alignedeuclidean)) * S ((cf_old_b_bound_alignedeuclidean) + (cf_tail_bound_alignedeuclidean)) + ((cf_tail_bound_alignedeuclidean) + (cf_tail_bound_alignedeuclidean))))))) /\ ((((exists ff_h_cf_bound_alignedeuclidean_following_state. ff_h_cf_bound_alignedeuclidean_following_state + S (((cf_new_a_bound_alignedeuclidean) + (((cf_new_b_bound_alignedeuclidean) + (cf_head_bound_alignedeuclidean)) * S ((cf_new_b_bound_alignedeuclidean) + (cf_head_bound_alignedeuclidean)) + ((cf_head_bound_alignedeuclidean) + (cf_head_bound_alignedeuclidean)))) * S ((cf_new_a_bound_alignedeuclidean) + (((cf_new_b_bound_alignedeuclidean) + (cf_head_bound_alignedeuclidean)) * S ((cf_new_b_bound_alignedeuclidean) + (cf_head_bound_alignedeuclidean)) + ((cf_head_bound_alignedeuclidean) + (cf_head_bound_alignedeuclidean)))) + ((((cf_new_b_bound_alignedeuclidean) + (cf_head_bound_alignedeuclidean)) * S ((cf_new_b_bound_alignedeuclidean) + (cf_head_bound_alignedeuclidean)) + ((cf_head_bound_alignedeuclidean) + (cf_head_bound_alignedeuclidean))) + (((cf_new_b_bound_alignedeuclidean) + (cf_head_bound_alignedeuclidean)) * S ((cf_new_b_bound_alignedeuclidean) + (cf_head_bound_alignedeuclidean)) + ((cf_head_bound_alignedeuclidean) + (cf_head_bound_alignedeuclidean))))) = S ((S (S cf_index_bound_alignedeuclidean)) * e)) /\ exists ff_q_cf_bound_alignedeuclidean_following_state. h = ff_q_cf_bound_alignedeuclidean_following_state * S ((S (S cf_index_bound_alignedeuclidean)) * e) + (((cf_new_a_bound_alignedeuclidean) + (((cf_new_b_bound_alignedeuclidean) + (cf_head_bound_alignedeuclidean)) * S ((cf_new_b_bound_alignedeuclidean) + (cf_head_bound_alignedeuclidean)) + ((cf_head_bound_alignedeuclidean) + (cf_head_bound_alignedeuclidean)))) * S ((cf_new_a_bound_alignedeuclidean) + (((cf_new_b_bound_alignedeuclidean) + (cf_head_bound_alignedeuclidean)) * S ((cf_new_b_bound_alignedeuclidean) + (cf_head_bound_alignedeuclidean)) + ((cf_head_bound_alignedeuclidean) + (cf_head_bound_alignedeuclidean)))) + ((((cf_new_b_bound_alignedeuclidean) + (cf_head_bound_alignedeuclidean)) * S ((cf_new_b_bound_alignedeuclidean) + (cf_head_bound_alignedeuclidean)) + ((cf_head_bound_alignedeuclidean) + (cf_head_bound_alignedeuclidean))) + (((cf_new_b_bound_alignedeuclidean) + (cf_head_bound_alignedeuclidean)) * S ((cf_new_b_bound_alignedeuclidean) + (cf_head_bound_alignedeuclidean)) + ((cf_head_bound_alignedeuclidean) + (cf_head_bound_alignedeuclidean))))))) /\ (cf_new_b_bound_alignedeuclidean = cf_old_a_bound_alignedeuclidean /\ (cf_new_a_bound_alignedeuclidean = cf_new_b_bound_alignedeuclidean * cf_quotient_bound_alignedeuclidean + cf_old_b_bound_alignedeuclidean /\ ((exists ff_lt_cf_bound_alignedeuclidean_remainder. ff_lt_cf_bound_alignedeuclidean_remainder + S cf_old_b_bound_alignedeuclidean = cf_new_b_bound_alignedeuclidean) /\ (cf_head_bound_alignedeuclidean = S ((cf_quotient_bound_alignedeuclidean + cf_tail_bound_alignedeuclidean) * S (cf_quotient_bound_alignedeuclidean + cf_tail_bound_alignedeuclidean) + (cf_tail_bound_alignedeuclidean + cf_tail_bound_alignedeuclidean))))))))))) /\ ((exists cfc_tail_bound_alignedmatrix. ((exists cfc_state_bound_alignedmatrixinitial. ((exists cfc_left_bound_alignedmatrixinitialcode cfc_right_bound_alignedmatrixinitialcode cfc_matrix_bound_alignedmatrixinitialcode. ((cfc_left_bound_alignedmatrixinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_bound_alignedmatrixinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_bound_alignedmatrixinitialcode = ((cfc_left_bound_alignedmatrixinitialcode) + (cfc_right_bound_alignedmatrixinitialcode)) * S ((cfc_left_bound_alignedmatrixinitialcode) + (cfc_right_bound_alignedmatrixinitialcode)) + ((cfc_right_bound_alignedmatrixinitialcode) + (cfc_right_bound_alignedmatrixinitialcode))) /\ ((cfc_state_bound_alignedmatrixinitial) = ((cfc_tail_bound_alignedmatrix) + (cfc_matrix_bound_alignedmatrixinitialcode)) * S ((cfc_tail_bound_alignedmatrix) + (cfc_matrix_bound_alignedmatrixinitialcode)) + ((cfc_matrix_bound_alignedmatrixinitialcode) + (cfc_matrix_bound_alignedmatrixinitialcode))))))) /\ (((exists ff_h_bound_alignedmatrixinitialentry. ff_h_bound_alignedmatrixinitialentry + S (cfc_state_bound_alignedmatrixinitial) = S ((S (0)) * E)) /\ exists ff_q_bound_alignedmatrixinitialentry. H = ff_q_bound_alignedmatrixinitialentry * S ((S (0)) * E) + (cfc_state_bound_alignedmatrixinitial))))) /\ ((exists cfc_state_bound_alignedmatrixterminal. ((exists cfc_left_bound_alignedmatrixterminalcode cfc_right_bound_alignedmatrixterminalcode cfc_matrix_bound_alignedmatrixterminalcode. ((cfc_left_bound_alignedmatrixterminalcode = ((cfc_p_bound_aligned) + (cfc_P_bound_aligned)) * S ((cfc_p_bound_aligned) + (cfc_P_bound_aligned)) + ((cfc_P_bound_aligned) + (cfc_P_bound_aligned))) /\ ((cfc_right_bound_alignedmatrixterminalcode = ((cfc_n_bound_aligned) + (cfc_N_bound_aligned)) * S ((cfc_n_bound_aligned) + (cfc_N_bound_aligned)) + ((cfc_N_bound_aligned) + (cfc_N_bound_aligned))) /\ ((cfc_matrix_bound_alignedmatrixterminalcode = ((cfc_left_bound_alignedmatrixterminalcode) + (cfc_right_bound_alignedmatrixterminalcode)) * S ((cfc_left_bound_alignedmatrixterminalcode) + (cfc_right_bound_alignedmatrixterminalcode)) + ((cfc_right_bound_alignedmatrixterminalcode) + (cfc_right_bound_alignedmatrixterminalcode))) /\ ((cfc_state_bound_alignedmatrixterminal) = ((cfc_tail_bound_aligned) + (cfc_matrix_bound_alignedmatrixterminalcode)) * S ((cfc_tail_bound_aligned) + (cfc_matrix_bound_alignedmatrixterminalcode)) + ((cfc_matrix_bound_alignedmatrixterminalcode) + (cfc_matrix_bound_alignedmatrixterminalcode))))))) /\ (((exists ff_h_bound_alignedmatrixterminalentry. ff_h_bound_alignedmatrixterminalentry + S (cfc_state_bound_alignedmatrixterminal) = S ((S (k)) * E)) /\ exists ff_q_bound_alignedmatrixterminalentry. H = ff_q_bound_alignedmatrixterminalentry * S ((S (k)) * E) + (cfc_state_bound_alignedmatrixterminal))))) /\ (forall cfc_index_bound_alignedmatrix. (exists cfba_gap_bound_alignedmatrixbound. cfba_gap_bound_alignedmatrixbound + S (cfc_index_bound_alignedmatrix) = (k)) -> exists cfc_old_bound_alignedmatrix cfc_a_bound_alignedmatrix cfc_b_bound_alignedmatrix cfc_c_bound_alignedmatrix cfc_d_bound_alignedmatrix cfc_new_bound_alignedmatrix cfc_quotient_bound_alignedmatrix. ((exists cfc_state_bound_alignedmatrixprevious. ((exists cfc_left_bound_alignedmatrixpreviouscode cfc_right_bound_alignedmatrixpreviouscode cfc_matrix_bound_alignedmatrixpreviouscode. ((cfc_left_bound_alignedmatrixpreviouscode = ((cfc_a_bound_alignedmatrix) + (cfc_b_bound_alignedmatrix)) * S ((cfc_a_bound_alignedmatrix) + (cfc_b_bound_alignedmatrix)) + ((cfc_b_bound_alignedmatrix) + (cfc_b_bound_alignedmatrix))) /\ ((cfc_right_bound_alignedmatrixpreviouscode = ((cfc_c_bound_alignedmatrix) + (cfc_d_bound_alignedmatrix)) * S ((cfc_c_bound_alignedmatrix) + (cfc_d_bound_alignedmatrix)) + ((cfc_d_bound_alignedmatrix) + (cfc_d_bound_alignedmatrix))) /\ ((cfc_matrix_bound_alignedmatrixpreviouscode = ((cfc_left_bound_alignedmatrixpreviouscode) + (cfc_right_bound_alignedmatrixpreviouscode)) * S ((cfc_left_bound_alignedmatrixpreviouscode) + (cfc_right_bound_alignedmatrixpreviouscode)) + ((cfc_right_bound_alignedmatrixpreviouscode) + (cfc_right_bound_alignedmatrixpreviouscode))) /\ ((cfc_state_bound_alignedmatrixprevious) = ((cfc_old_bound_alignedmatrix) + (cfc_matrix_bound_alignedmatrixpreviouscode)) * S ((cfc_old_bound_alignedmatrix) + (cfc_matrix_bound_alignedmatrixpreviouscode)) + ((cfc_matrix_bound_alignedmatrixpreviouscode) + (cfc_matrix_bound_alignedmatrixpreviouscode))))))) /\ (((exists ff_h_bound_alignedmatrixpreviousentry. ff_h_bound_alignedmatrixpreviousentry + S (cfc_state_bound_alignedmatrixprevious) = S ((S (cfc_index_bound_alignedmatrix)) * E)) /\ exists ff_q_bound_alignedmatrixpreviousentry. H = ff_q_bound_alignedmatrixpreviousentry * S ((S (cfc_index_bound_alignedmatrix)) * E) + (cfc_state_bound_alignedmatrixprevious))))) /\ ((exists cfc_state_bound_alignedmatrixfollowing. ((exists cfc_left_bound_alignedmatrixfollowingcode cfc_right_bound_alignedmatrixfollowingcode cfc_matrix_bound_alignedmatrixfollowingcode. ((cfc_left_bound_alignedmatrixfollowingcode = (((cfc_quotient_bound_alignedmatrix * cfc_a_bound_alignedmatrix + cfc_c_bound_alignedmatrix)) + ((cfc_quotient_bound_alignedmatrix * cfc_b_bound_alignedmatrix + cfc_d_bound_alignedmatrix))) * S (((cfc_quotient_bound_alignedmatrix * cfc_a_bound_alignedmatrix + cfc_c_bound_alignedmatrix)) + ((cfc_quotient_bound_alignedmatrix * cfc_b_bound_alignedmatrix + cfc_d_bound_alignedmatrix))) + (((cfc_quotient_bound_alignedmatrix * cfc_b_bound_alignedmatrix + cfc_d_bound_alignedmatrix)) + ((cfc_quotient_bound_alignedmatrix * cfc_b_bound_alignedmatrix + cfc_d_bound_alignedmatrix)))) /\ ((cfc_right_bound_alignedmatrixfollowingcode = ((cfc_a_bound_alignedmatrix) + (cfc_b_bound_alignedmatrix)) * S ((cfc_a_bound_alignedmatrix) + (cfc_b_bound_alignedmatrix)) + ((cfc_b_bound_alignedmatrix) + (cfc_b_bound_alignedmatrix))) /\ ((cfc_matrix_bound_alignedmatrixfollowingcode = ((cfc_left_bound_alignedmatrixfollowingcode) + (cfc_right_bound_alignedmatrixfollowingcode)) * S ((cfc_left_bound_alignedmatrixfollowingcode) + (cfc_right_bound_alignedmatrixfollowingcode)) + ((cfc_right_bound_alignedmatrixfollowingcode) + (cfc_right_bound_alignedmatrixfollowingcode))) /\ ((cfc_state_bound_alignedmatrixfollowing) = ((cfc_new_bound_alignedmatrix) + (cfc_matrix_bound_alignedmatrixfollowingcode)) * S ((cfc_new_bound_alignedmatrix) + (cfc_matrix_bound_alignedmatrixfollowingcode)) + ((cfc_matrix_bound_alignedmatrixfollowingcode) + (cfc_matrix_bound_alignedmatrixfollowingcode))))))) /\ (((exists ff_h_bound_alignedmatrixfollowingentry. ff_h_bound_alignedmatrixfollowingentry + S (cfc_state_bound_alignedmatrixfollowing) = S ((S (S cfc_index_bound_alignedmatrix)) * E)) /\ exists ff_q_bound_alignedmatrixfollowingentry. H = ff_q_bound_alignedmatrixfollowingentry * S ((S (S cfc_index_bound_alignedmatrix)) * E) + (cfc_state_bound_alignedmatrixfollowing))))) /\ (cfc_new_bound_alignedmatrix = S ((cfc_quotient_bound_alignedmatrix + cfc_old_bound_alignedmatrix) * S (cfc_quotient_bound_alignedmatrix + cfc_old_bound_alignedmatrix) + (cfc_old_bound_alignedmatrix + cfc_old_bound_alignedmatrix))))))))) /\ (((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