BA003F

cf_convergent_every_valid_matrix_prefix_exists

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

HA induction on the actual complete Euclidean history constructs every valid quotient-matrix prefix, including the empty, initial, and full terminal products.

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 L k a b s h e. (exists cf_gcd_complete_source. ((((exists ff_h_cf_complete_source_initial_state. ff_h_cf_complete_source_initial_state + S (((cf_gcd_complete_source) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_complete_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_complete_source_initial_state. h = ff_q_cf_complete_source_initial_state * S ((S (0)) * e) + (((cf_gcd_complete_source) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_complete_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_complete_source_terminal_state. ff_h_cf_complete_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_complete_source_terminal_state. h = ff_q_cf_complete_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_complete_source. (exists ff_lt_cf_complete_source_index. ff_lt_cf_complete_source_index + S cf_index_complete_source = L) -> exists cf_old_a_complete_source cf_old_b_complete_source cf_tail_complete_source cf_new_a_complete_source cf_new_b_complete_source cf_head_complete_source cf_quotient_complete_source. ((((exists ff_h_cf_complete_source_previous_state. ff_h_cf_complete_source_previous_state + S (((cf_old_a_complete_source) + (((cf_old_b_complete_source) + (cf_tail_complete_source)) * S ((cf_old_b_complete_source) + (cf_tail_complete_source)) + ((cf_tail_complete_source) + (cf_tail_complete_source)))) * S ((cf_old_a_complete_source) + (((cf_old_b_complete_source) + (cf_tail_complete_source)) * S ((cf_old_b_complete_source) + (cf_tail_complete_source)) + ((cf_tail_complete_source) + (cf_tail_complete_source)))) + ((((cf_old_b_complete_source) + (cf_tail_complete_source)) * S ((cf_old_b_complete_source) + (cf_tail_complete_source)) + ((cf_tail_complete_source) + (cf_tail_complete_source))) + (((cf_old_b_complete_source) + (cf_tail_complete_source)) * S ((cf_old_b_complete_source) + (cf_tail_complete_source)) + ((cf_tail_complete_source) + (cf_tail_complete_source))))) = S ((S (cf_index_complete_source)) * e)) /\ exists ff_q_cf_complete_source_previous_state. h = ff_q_cf_complete_source_previous_state * S ((S (cf_index_complete_source)) * e) + (((cf_old_a_complete_source) + (((cf_old_b_complete_source) + (cf_tail_complete_source)) * S ((cf_old_b_complete_source) + (cf_tail_complete_source)) + ((cf_tail_complete_source) + (cf_tail_complete_source)))) * S ((cf_old_a_complete_source) + (((cf_old_b_complete_source) + (cf_tail_complete_source)) * S ((cf_old_b_complete_source) + (cf_tail_complete_source)) + ((cf_tail_complete_source) + (cf_tail_complete_source)))) + ((((cf_old_b_complete_source) + (cf_tail_complete_source)) * S ((cf_old_b_complete_source) + (cf_tail_complete_source)) + ((cf_tail_complete_source) + (cf_tail_complete_source))) + (((cf_old_b_complete_source) + (cf_tail_complete_source)) * S ((cf_old_b_complete_source) + (cf_tail_complete_source)) + ((cf_tail_complete_source) + (cf_tail_complete_source))))))) /\ ((((exists ff_h_cf_complete_source_following_state. ff_h_cf_complete_source_following_state + S (((cf_new_a_complete_source) + (((cf_new_b_complete_source) + (cf_head_complete_source)) * S ((cf_new_b_complete_source) + (cf_head_complete_source)) + ((cf_head_complete_source) + (cf_head_complete_source)))) * S ((cf_new_a_complete_source) + (((cf_new_b_complete_source) + (cf_head_complete_source)) * S ((cf_new_b_complete_source) + (cf_head_complete_source)) + ((cf_head_complete_source) + (cf_head_complete_source)))) + ((((cf_new_b_complete_source) + (cf_head_complete_source)) * S ((cf_new_b_complete_source) + (cf_head_complete_source)) + ((cf_head_complete_source) + (cf_head_complete_source))) + (((cf_new_b_complete_source) + (cf_head_complete_source)) * S ((cf_new_b_complete_source) + (cf_head_complete_source)) + ((cf_head_complete_source) + (cf_head_complete_source))))) = S ((S (S cf_index_complete_source)) * e)) /\ exists ff_q_cf_complete_source_following_state. h = ff_q_cf_complete_source_following_state * S ((S (S cf_index_complete_source)) * e) + (((cf_new_a_complete_source) + (((cf_new_b_complete_source) + (cf_head_complete_source)) * S ((cf_new_b_complete_source) + (cf_head_complete_source)) + ((cf_head_complete_source) + (cf_head_complete_source)))) * S ((cf_new_a_complete_source) + (((cf_new_b_complete_source) + (cf_head_complete_source)) * S ((cf_new_b_complete_source) + (cf_head_complete_source)) + ((cf_head_complete_source) + (cf_head_complete_source)))) + ((((cf_new_b_complete_source) + (cf_head_complete_source)) * S ((cf_new_b_complete_source) + (cf_head_complete_source)) + ((cf_head_complete_source) + (cf_head_complete_source))) + (((cf_new_b_complete_source) + (cf_head_complete_source)) * S ((cf_new_b_complete_source) + (cf_head_complete_source)) + ((cf_head_complete_source) + (cf_head_complete_source))))))) /\ (cf_new_b_complete_source = cf_old_a_complete_source /\ (cf_new_a_complete_source = cf_new_b_complete_source * cf_quotient_complete_source + cf_old_b_complete_source /\ ((exists ff_lt_cf_complete_source_remainder. ff_lt_cf_complete_source_remainder + S cf_old_b_complete_source = cf_new_b_complete_source) /\ (cf_head_complete_source = S ((cf_quotient_complete_source + cf_tail_complete_source) * S (cf_quotient_complete_source + cf_tail_complete_source) + (cf_tail_complete_source + cf_tail_complete_source))))))))))) -> (exists cfba_bound_complete_index. cfba_bound_complete_index + (k) = (L)) -> (exists cfc_h_complete_result cfc_e_complete_result cfc_u_complete_result cfc_U_complete_result cfc_v_complete_result cfc_V_complete_result. exists cfc_tail_complete_resultbody. ((exists cfc_state_complete_resultbodyinitial. ((exists cfc_left_complete_resultbodyinitialcode cfc_right_complete_resultbodyinitialcode cfc_matrix_complete_resultbodyinitialcode. ((cfc_left_complete_resultbodyinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_complete_resultbodyinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_complete_resultbodyinitialcode = ((cfc_left_complete_resultbodyinitialcode) + (cfc_right_complete_resultbodyinitialcode)) * S ((cfc_left_complete_resultbodyinitialcode) + (cfc_right_complete_resultbodyinitialcode)) + ((cfc_right_complete_resultbodyinitialcode) + (cfc_right_complete_resultbodyinitialcode))) /\ ((cfc_state_complete_resultbodyinitial) = ((cfc_tail_complete_resultbody) + (cfc_matrix_complete_resultbodyinitialcode)) * S ((cfc_tail_complete_resultbody) + (cfc_matrix_complete_resultbodyinitialcode)) + ((cfc_matrix_complete_resultbodyinitialcode) + (cfc_matrix_complete_resultbodyinitialcode))))))) /\ (((exists ff_h_complete_resultbodyinitialentry. ff_h_complete_resultbodyinitialentry + S (cfc_state_complete_resultbodyinitial) = S ((S (0)) * cfc_e_complete_result)) /\ exists ff_q_complete_resultbodyinitialentry. cfc_h_complete_result = ff_q_complete_resultbodyinitialentry * S ((S (0)) * cfc_e_complete_result) + (cfc_state_complete_resultbodyinitial))))) /\ ((exists cfc_state_complete_resultbodyterminal. ((exists cfc_left_complete_resultbodyterminalcode cfc_right_complete_resultbodyterminalcode cfc_matrix_complete_resultbodyterminalcode. ((cfc_left_complete_resultbodyterminalcode = ((cfc_u_complete_result) + (cfc_U_complete_result)) * S ((cfc_u_complete_result) + (cfc_U_complete_result)) + ((cfc_U_complete_result) + (cfc_U_complete_result))) /\ ((cfc_right_complete_resultbodyterminalcode = ((cfc_v_complete_result) + (cfc_V_complete_result)) * S ((cfc_v_complete_result) + (cfc_V_complete_result)) + ((cfc_V_complete_result) + (cfc_V_complete_result))) /\ ((cfc_matrix_complete_resultbodyterminalcode = ((cfc_left_complete_resultbodyterminalcode) + (cfc_right_complete_resultbodyterminalcode)) * S ((cfc_left_complete_resultbodyterminalcode) + (cfc_right_complete_resultbodyterminalcode)) + ((cfc_right_complete_resultbodyterminalcode) + (cfc_right_complete_resultbodyterminalcode))) /\ ((cfc_state_complete_resultbodyterminal) = ((s) + (cfc_matrix_complete_resultbodyterminalcode)) * S ((s) + (cfc_matrix_complete_resultbodyterminalcode)) + ((cfc_matrix_complete_resultbodyterminalcode) + (cfc_matrix_complete_resultbodyterminalcode))))))) /\ (((exists ff_h_complete_resultbodyterminalentry. ff_h_complete_resultbodyterminalentry + S (cfc_state_complete_resultbodyterminal) = S ((S (k)) * cfc_e_complete_result)) /\ exists ff_q_complete_resultbodyterminalentry. cfc_h_complete_result = ff_q_complete_resultbodyterminalentry * S ((S (k)) * cfc_e_complete_result) + (cfc_state_complete_resultbodyterminal))))) /\ (forall cfc_index_complete_resultbody. (exists cfba_gap_complete_resultbodybound. cfba_gap_complete_resultbodybound + S (cfc_index_complete_resultbody) = (k)) -> exists cfc_old_complete_resultbody cfc_a_complete_resultbody cfc_b_complete_resultbody cfc_c_complete_resultbody cfc_d_complete_resultbody cfc_new_complete_resultbody cfc_quotient_complete_resultbody. ((exists cfc_state_complete_resultbodyprevious. ((exists cfc_left_complete_resultbodypreviouscode cfc_right_complete_resultbodypreviouscode cfc_matrix_complete_resultbodypreviouscode. ((cfc_left_complete_resultbodypreviouscode = ((cfc_a_complete_resultbody) + (cfc_b_complete_resultbody)) * S ((cfc_a_complete_resultbody) + (cfc_b_complete_resultbody)) + ((cfc_b_complete_resultbody) + (cfc_b_complete_resultbody))) /\ ((cfc_right_complete_resultbodypreviouscode = ((cfc_c_complete_resultbody) + (cfc_d_complete_resultbody)) * S ((cfc_c_complete_resultbody) + (cfc_d_complete_resultbody)) + ((cfc_d_complete_resultbody) + (cfc_d_complete_resultbody))) /\ ((cfc_matrix_complete_resultbodypreviouscode = ((cfc_left_complete_resultbodypreviouscode) + (cfc_right_complete_resultbodypreviouscode)) * S ((cfc_left_complete_resultbodypreviouscode) + (cfc_right_complete_resultbodypreviouscode)) + ((cfc_right_complete_resultbodypreviouscode) + (cfc_right_complete_resultbodypreviouscode))) /\ ((cfc_state_complete_resultbodyprevious) = ((cfc_old_complete_resultbody) + (cfc_matrix_complete_resultbodypreviouscode)) * S ((cfc_old_complete_resultbody) + (cfc_matrix_complete_resultbodypreviouscode)) + ((cfc_matrix_complete_resultbodypreviouscode) + (cfc_matrix_complete_resultbodypreviouscode))))))) /\ (((exists ff_h_complete_resultbodypreviousentry. ff_h_complete_resultbodypreviousentry + S (cfc_state_complete_resultbodyprevious) = S ((S (cfc_index_complete_resultbody)) * cfc_e_complete_result)) /\ exists ff_q_complete_resultbodypreviousentry. cfc_h_complete_result = ff_q_complete_resultbodypreviousentry * S ((S (cfc_index_complete_resultbody)) * cfc_e_complete_result) + (cfc_state_complete_resultbodyprevious))))) /\ ((exists cfc_state_complete_resultbodyfollowing. ((exists cfc_left_complete_resultbodyfollowingcode cfc_right_complete_resultbodyfollowingcode cfc_matrix_complete_resultbodyfollowingcode. ((cfc_left_complete_resultbodyfollowingcode = (((cfc_quotient_complete_resultbody * cfc_a_complete_resultbody + cfc_c_complete_resultbody)) + ((cfc_quotient_complete_resultbody * cfc_b_complete_resultbody + cfc_d_complete_resultbody))) * S (((cfc_quotient_complete_resultbody * cfc_a_complete_resultbody + cfc_c_complete_resultbody)) + ((cfc_quotient_complete_resultbody * cfc_b_complete_resultbody + cfc_d_complete_resultbody))) + (((cfc_quotient_complete_resultbody * cfc_b_complete_resultbody + cfc_d_complete_resultbody)) + ((cfc_quotient_complete_resultbody * cfc_b_complete_resultbody + cfc_d_complete_resultbody)))) /\ ((cfc_right_complete_resultbodyfollowingcode = ((cfc_a_complete_resultbody) + (cfc_b_complete_resultbody)) * S ((cfc_a_complete_resultbody) + (cfc_b_complete_resultbody)) + ((cfc_b_complete_resultbody) + (cfc_b_complete_resultbody))) /\ ((cfc_matrix_complete_resultbodyfollowingcode = ((cfc_left_complete_resultbodyfollowingcode) + (cfc_right_complete_resultbodyfollowingcode)) * S ((cfc_left_complete_resultbodyfollowingcode) + (cfc_right_complete_resultbodyfollowingcode)) + ((cfc_right_complete_resultbodyfollowingcode) + (cfc_right_complete_resultbodyfollowingcode))) /\ ((cfc_state_complete_resultbodyfollowing) = ((cfc_new_complete_resultbody) + (cfc_matrix_complete_resultbodyfollowingcode)) * S ((cfc_new_complete_resultbody) + (cfc_matrix_complete_resultbodyfollowingcode)) + ((cfc_matrix_complete_resultbodyfollowingcode) + (cfc_matrix_complete_resultbodyfollowingcode))))))) /\ (((exists ff_h_complete_resultbodyfollowingentry. ff_h_complete_resultbodyfollowingentry + S (cfc_state_complete_resultbodyfollowing) = S ((S (S cfc_index_complete_resultbody)) * cfc_e_complete_result)) /\ exists ff_q_complete_resultbodyfollowingentry. cfc_h_complete_result = ff_q_complete_resultbodyfollowingentry * S ((S (S cfc_index_complete_resultbody)) * cfc_e_complete_result) + (cfc_state_complete_resultbodyfollowing))))) /\ (cfc_new_complete_resultbody = S ((cfc_quotient_complete_resultbody + cfc_old_complete_resultbody) * S (cfc_quotient_complete_resultbody + cfc_old_complete_resultbody) + (cfc_old_complete_resultbody + cfc_old_complete_resultbody)))))))))

Constructive proof overview

Generated structural guide

HA induction on the actual complete Euclidean history constructs every valid quotient-matrix prefix, including the empty, initial, and full terminal products.

The unchanged tactic script uses 7 declared prerequisites and contains 144 exact native proof lines.

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

Proof neighborhood

Direct dependencies

le_zero Stable theorem; checked-use authorized zero_or_succ Stable theorem; checked-use authorized BA003A cf_convergent_matrix_empty_exists BA0036 cf_convergent_matrix_length_transport BA002A cf_convergent_old_history_successor_elimination le_of_succ_le_succ Stable theorem; checked-use authorized BA003C cf_convergent_matrix_prepend_exists

Direct dependents

BA0041 continued_fraction_convergent_exists_at_history_index

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

144 script commands · 32 reading checkpoints · 7 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 (4)
cf convergent matrix empty existscf convergent matrix length transportcf convergent old history successor eliminationcf convergent matrix prepend exists

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 LL1–9

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

  1. L1
    induction L
  2. L2
    intro k
  3. L3
    intro a
  4. L4
    intro b
  5. L5
    intro s
  6. L6
    intro h
  7. L7
    intro e
  8. L8
    intro ht
  9. L9
    intro hk
02Establish hkzeroL10–13

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

  1. L10
    have hkzero : k = 0
  2. L11
    specialize le_zero (k)
  3. L12
    apply le_zero
  4. L13
    exact hk
03Establish hzL14–16

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

  1. L14
    have hz : ∃ H. ∃ E. ConvergentMatrixTrace(s,H,E,0,1,0,0,1)Definitions: ConvergentMatrixTrace
  2. L15
    specialize cf_convergent_matrix_empty_exists (s)
  3. L16
    apply cf_convergent_matrix_empty_exists
04Separate the logical casesL17–18

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

  1. L17
    cases hz
  2. L18
    cases hz_witness
05Construct an explicit witnessL19–24

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

  1. L19
    exists x
  2. L20
    exists x1
  3. L21
    exists 1
  4. L22
    exists 0
  5. L23
    exists 0
  6. L24
    exists 1
06Use earlier factsL25–34

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

  1. L25
    specialize cf_convergent_matrix_length_transport (s)
  2. L26
    specialize cf_convergent_matrix_length_transport (x)
  3. L27
    specialize cf_convergent_matrix_length_transport (x1)
  4. L28
    specialize cf_convergent_matrix_length_transport (0)
  5. L29
    specialize cf_convergent_matrix_length_transport (k)
  6. L30
    specialize cf_convergent_matrix_length_transport (1)
  7. L31
    specialize cf_convergent_matrix_length_transport (0)
  8. L32
    specialize cf_convergent_matrix_length_transport (0)
  9. L33
    specialize cf_convergent_matrix_length_transport (1)
  10. L34
    apply cf_convergent_matrix_length_transport
07Calculate and transport equalitiesL35–35

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

  1. L35
    symm
08Use earlier factsL36–37

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

  1. L36
    exact hkzero
  2. L37
    exact hz_witness_witness
09Fix variables and assumptionsL38–45

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

  1. L38
    intro k
  2. L39
    intro a
  3. L40
    intro b
  4. L41
    intro s
  5. L42
    intro h
  6. L43
    intro e
  7. L44
    intro ht
  8. L45
    intro hk
10Establish hkcaseL46–48

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

  1. L46
    have hkcase : k = 0 \/ exists i. k = S i
  2. L47
    specialize zero_or_succ (k)
  3. L48
    apply zero_or_succ
11Separate the logical casesL49–49

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

  1. L49
    cases hkcase
12Establish hzL50–52

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

  1. L50
    have hz : ∃ H. ∃ E. ConvergentMatrixTrace(s,H,E,0,1,0,0,1)Definitions: ConvergentMatrixTrace
  2. L51
    specialize cf_convergent_matrix_empty_exists (s)
  3. L52
    apply cf_convergent_matrix_empty_exists
13Separate the logical casesL53–54

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

  1. L53
    cases hz
  2. L54
    cases hz_witness
14Construct an explicit witnessL55–60

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

  1. L55
    exists x
  2. L56
    exists x1
  3. L57
    exists 1
  4. L58
    exists 0
  5. L59
    exists 0
  6. L60
    exists 1
15Use earlier factsL61–70

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

  1. L61
    specialize cf_convergent_matrix_length_transport (s)
  2. L62
    specialize cf_convergent_matrix_length_transport (x)
  3. L63
    specialize cf_convergent_matrix_length_transport (x1)
  4. L64
    specialize cf_convergent_matrix_length_transport (0)
  5. L65
    specialize cf_convergent_matrix_length_transport (k)
  6. L66
    specialize cf_convergent_matrix_length_transport (1)
  7. L67
    specialize cf_convergent_matrix_length_transport (0)
  8. L68
    specialize cf_convergent_matrix_length_transport (0)
  9. L69
    specialize cf_convergent_matrix_length_transport (1)
  10. L70
    apply cf_convergent_matrix_length_transport
16Calculate and transport equalitiesL71–71

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

  1. L71
    symm
17Use earlier factsL72–73

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

  1. L72
    exact hkcase_left
  2. L73
    exact hz_witness_witness
18Separate the logical casesL74–74

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

  1. L74
    cases hkcase_right
19Establish hpL75–83

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

  1. L75
    have hp : ∃ q. ∃ r. ∃ t. a = b · q + r ∧ (Lt(r,b) ∧ (ListCell(s,q,t) ∧ ContinuedFractionTrace(b,r,t,h,e,L)))Definitions: ListCellContinuedFractionTraceLt
  2. L76
    specialize cf_convergent_old_history_successor_elimination (a)
  3. L77
    specialize cf_convergent_old_history_successor_elimination (b)
  4. L78
    specialize cf_convergent_old_history_successor_elimination (s)
  5. L79
    specialize cf_convergent_old_history_successor_elimination (h)
  6. L80
    specialize cf_convergent_old_history_successor_elimination (e)
  7. L81
    specialize cf_convergent_old_history_successor_elimination (L)
  8. L82
    apply cf_convergent_old_history_successor_elimination
  9. L83
    exact ht
20Separate the logical casesL84–89

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

  1. L84
    cases hp
  2. L85
    cases hp_witness
  3. L86
    cases hp_witness_witness
  4. L87
    cases hp_witness_witness_witness
  5. L88
    cases hp_witness_witness_witness_right
  6. L89
    cases hp_witness_witness_witness_right_right
21Establish hcL90–99

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

  1. L90
    have hc : ∃ cfc_h_complete_child. ∃ cfc_e_complete_child. ∃ cfc_u_complete_child. ∃ cfc_U_complete_child. ∃ cfc_v_complete_child. ∃ cfc_V_complete_child. ConvergentMatrixTrace(x3,cfc_h_complete_child,cfc_e_complete_child,x,cfc_u_complete_child,cfc_U_complete_child,cfc_v_complete_child,cfc_V_complete_child)Definitions: ConvergentMatrixTrace
  2. L91
    specialize IH (x)
  3. L92
    specialize IH (b)
  4. L93
    specialize IH (x2)
  5. L94
    specialize IH (x3)
  6. L95
    specialize IH (h)
  7. L96
    specialize IH (e)
  8. L97
    apply IH
  9. L98
    exact hp_witness_witness_witness_right_right_right
  10. L99
    specialize le_of_succ_le_succ (x)
22Use earlier factsL100–101

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

  1. L100
    specialize le_of_succ_le_succ (L)
  2. L101
    apply le_of_succ_le_succ
23Calculate and transport equalitiesL102–102

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

  1. L102
    rewrite <- hkcase_right_witness
24Use earlier factsL103–103

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

  1. L103
    exact hk
25Separate the logical casesL104–109

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

  1. L104
    cases hc
  2. L105
    cases hc_witness
  3. L106
    cases hc_witness_witness
  4. L107
    cases hc_witness_witness_witness
  5. L108
    cases hc_witness_witness_witness_witness
  6. L109
    cases hc_witness_witness_witness_witness_witness
26Establish hextL110–119

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

  1. L110
    have hext : ∃ H. ∃ E. ConvergentMatrixTrace(s,H,E,S x,x1 · x6 + x8,x1 · x7 + x9,x6,x7)Definitions: ConvergentMatrixTrace
  2. L111
    specialize cf_convergent_matrix_prepend_exists (x3)
  3. L112
    specialize cf_convergent_matrix_prepend_exists (x4)
  4. L113
    specialize cf_convergent_matrix_prepend_exists (x5)
  5. L114
    specialize cf_convergent_matrix_prepend_exists (x)
  6. L115
    specialize cf_convergent_matrix_prepend_exists (x6)
  7. L116
    specialize cf_convergent_matrix_prepend_exists (x7)
  8. L117
    specialize cf_convergent_matrix_prepend_exists (x8)
  9. L118
    specialize cf_convergent_matrix_prepend_exists (x9)
  10. L119
    specialize cf_convergent_matrix_prepend_exists (x1)
27Use earlier factsL120–123

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

  1. L120
    specialize cf_convergent_matrix_prepend_exists (s)
  2. L121
    apply cf_convergent_matrix_prepend_exists
  3. L122
    exact hc_witness_witness_witness_witness_witness_witness
  4. L123
    exact hp_witness_witness_witness_right_right_left
28Separate the logical casesL124–125

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

  1. L124
    cases hext
  2. L125
    cases hext_witness
29Construct an explicit witnessL126–131

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

  1. L126
    exists x10
  2. L127
    exists x11
  3. L128
    exists x1 * x6 + x8
  4. L129
    exists x1 * x7 + x9
  5. L130
    exists x6
  6. L131
    exists x7
30Use earlier factsL132–141

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

  1. L132
    specialize cf_convergent_matrix_length_transport (s)
  2. L133
    specialize cf_convergent_matrix_length_transport (x10)
  3. L134
    specialize cf_convergent_matrix_length_transport (x11)
  4. L135
    specialize cf_convergent_matrix_length_transport (S x)
  5. L136
    specialize cf_convergent_matrix_length_transport (k)
  6. L137
    specialize cf_convergent_matrix_length_transport (x1 * x6 + x8)
  7. L138
    specialize cf_convergent_matrix_length_transport (x1 * x7 + x9)
  8. L139
    specialize cf_convergent_matrix_length_transport (x6)
  9. L140
    specialize cf_convergent_matrix_length_transport (x7)
  10. L141
    apply cf_convergent_matrix_length_transport
31Calculate and transport equalitiesL142–142

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

  1. L142
    symm
32Use earlier factsL143–144

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

  1. L143
    exact hkcase_right_witness
  2. L144
    exact hext_witness_witness

Library-wide reading audit

Original exact command ledger · 144 lines
  1. 0001induction L
  2. 0002intro k
  3. 0003intro a
  4. 0004intro b
  5. 0005intro s
  6. 0006intro h
  7. 0007intro e
  8. 0008intro ht
  9. 0009intro hk
  10. 0010have hkzero : k = 0
  11. 0011specialize le_zero (k)
  12. 0012apply le_zero
  13. 0013exact hk
  14. 0014have hz : exists H E. exists cfc_tail_complete_empty. ((exists cfc_state_complete_emptyinitial. ((exists cfc_left_complete_emptyinitialcode cfc_right_complete_emptyinitialcode cfc_matrix_complete_emptyinitialcode. ((cfc_left_complete_emptyinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_complete_emptyinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_complete_emptyinitialcode = ((cfc_left_complete_emptyinitialcode) + (cfc_right_complete_emptyinitialcode)) * S ((cfc_left_complete_emptyinitialcode) + (cfc_right_complete_emptyinitialcode)) + ((cfc_right_complete_emptyinitialcode) + (cfc_right_complete_emptyinitialcode))) /\ ((cfc_state_complete_emptyinitial) = ((cfc_tail_complete_empty) + (cfc_matrix_complete_emptyinitialcode)) * S ((cfc_tail_complete_empty) + (cfc_matrix_complete_emptyinitialcode)) + ((cfc_matrix_complete_emptyinitialcode) + (cfc_matrix_complete_emptyinitialcode))))))) /\ (((exists ff_h_complete_emptyinitialentry. ff_h_complete_emptyinitialentry + S (cfc_state_complete_emptyinitial) = S ((S (0)) * E)) /\ exists ff_q_complete_emptyinitialentry. H = ff_q_complete_emptyinitialentry * S ((S (0)) * E) + (cfc_state_complete_emptyinitial))))) /\ ((exists cfc_state_complete_emptyterminal. ((exists cfc_left_complete_emptyterminalcode cfc_right_complete_emptyterminalcode cfc_matrix_complete_emptyterminalcode. ((cfc_left_complete_emptyterminalcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_complete_emptyterminalcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_complete_emptyterminalcode = ((cfc_left_complete_emptyterminalcode) + (cfc_right_complete_emptyterminalcode)) * S ((cfc_left_complete_emptyterminalcode) + (cfc_right_complete_emptyterminalcode)) + ((cfc_right_complete_emptyterminalcode) + (cfc_right_complete_emptyterminalcode))) /\ ((cfc_state_complete_emptyterminal) = ((s) + (cfc_matrix_complete_emptyterminalcode)) * S ((s) + (cfc_matrix_complete_emptyterminalcode)) + ((cfc_matrix_complete_emptyterminalcode) + (cfc_matrix_complete_emptyterminalcode))))))) /\ (((exists ff_h_complete_emptyterminalentry. ff_h_complete_emptyterminalentry + S (cfc_state_complete_emptyterminal) = S ((S (0)) * E)) /\ exists ff_q_complete_emptyterminalentry. H = ff_q_complete_emptyterminalentry * S ((S (0)) * E) + (cfc_state_complete_emptyterminal))))) /\ (forall cfc_index_complete_empty. (exists cfba_gap_complete_emptybound. cfba_gap_complete_emptybound + S (cfc_index_complete_empty) = (0)) -> exists cfc_old_complete_empty cfc_a_complete_empty cfc_b_complete_empty cfc_c_complete_empty cfc_d_complete_empty cfc_new_complete_empty cfc_quotient_complete_empty. ((exists cfc_state_complete_emptyprevious. ((exists cfc_left_complete_emptypreviouscode cfc_right_complete_emptypreviouscode cfc_matrix_complete_emptypreviouscode. ((cfc_left_complete_emptypreviouscode = ((cfc_a_complete_empty) + (cfc_b_complete_empty)) * S ((cfc_a_complete_empty) + (cfc_b_complete_empty)) + ((cfc_b_complete_empty) + (cfc_b_complete_empty))) /\ ((cfc_right_complete_emptypreviouscode = ((cfc_c_complete_empty) + (cfc_d_complete_empty)) * S ((cfc_c_complete_empty) + (cfc_d_complete_empty)) + ((cfc_d_complete_empty) + (cfc_d_complete_empty))) /\ ((cfc_matrix_complete_emptypreviouscode = ((cfc_left_complete_emptypreviouscode) + (cfc_right_complete_emptypreviouscode)) * S ((cfc_left_complete_emptypreviouscode) + (cfc_right_complete_emptypreviouscode)) + ((cfc_right_complete_emptypreviouscode) + (cfc_right_complete_emptypreviouscode))) /\ ((cfc_state_complete_emptyprevious) = ((cfc_old_complete_empty) + (cfc_matrix_complete_emptypreviouscode)) * S ((cfc_old_complete_empty) + (cfc_matrix_complete_emptypreviouscode)) + ((cfc_matrix_complete_emptypreviouscode) + (cfc_matrix_complete_emptypreviouscode))))))) /\ (((exists ff_h_complete_emptypreviousentry. ff_h_complete_emptypreviousentry + S (cfc_state_complete_emptyprevious) = S ((S (cfc_index_complete_empty)) * E)) /\ exists ff_q_complete_emptypreviousentry. H = ff_q_complete_emptypreviousentry * S ((S (cfc_index_complete_empty)) * E) + (cfc_state_complete_emptyprevious))))) /\ ((exists cfc_state_complete_emptyfollowing. ((exists cfc_left_complete_emptyfollowingcode cfc_right_complete_emptyfollowingcode cfc_matrix_complete_emptyfollowingcode. ((cfc_left_complete_emptyfollowingcode = (((cfc_quotient_complete_empty * cfc_a_complete_empty + cfc_c_complete_empty)) + ((cfc_quotient_complete_empty * cfc_b_complete_empty + cfc_d_complete_empty))) * S (((cfc_quotient_complete_empty * cfc_a_complete_empty + cfc_c_complete_empty)) + ((cfc_quotient_complete_empty * cfc_b_complete_empty + cfc_d_complete_empty))) + (((cfc_quotient_complete_empty * cfc_b_complete_empty + cfc_d_complete_empty)) + ((cfc_quotient_complete_empty * cfc_b_complete_empty + cfc_d_complete_empty)))) /\ ((cfc_right_complete_emptyfollowingcode = ((cfc_a_complete_empty) + (cfc_b_complete_empty)) * S ((cfc_a_complete_empty) + (cfc_b_complete_empty)) + ((cfc_b_complete_empty) + (cfc_b_complete_empty))) /\ ((cfc_matrix_complete_emptyfollowingcode = ((cfc_left_complete_emptyfollowingcode) + (cfc_right_complete_emptyfollowingcode)) * S ((cfc_left_complete_emptyfollowingcode) + (cfc_right_complete_emptyfollowingcode)) + ((cfc_right_complete_emptyfollowingcode) + (cfc_right_complete_emptyfollowingcode))) /\ ((cfc_state_complete_emptyfollowing) = ((cfc_new_complete_empty) + (cfc_matrix_complete_emptyfollowingcode)) * S ((cfc_new_complete_empty) + (cfc_matrix_complete_emptyfollowingcode)) + ((cfc_matrix_complete_emptyfollowingcode) + (cfc_matrix_complete_emptyfollowingcode))))))) /\ (((exists ff_h_complete_emptyfollowingentry. ff_h_complete_emptyfollowingentry + S (cfc_state_complete_emptyfollowing) = S ((S (S cfc_index_complete_empty)) * E)) /\ exists ff_q_complete_emptyfollowingentry. H = ff_q_complete_emptyfollowingentry * S ((S (S cfc_index_complete_empty)) * E) + (cfc_state_complete_emptyfollowing))))) /\ (cfc_new_complete_empty = S ((cfc_quotient_complete_empty + cfc_old_complete_empty) * S (cfc_quotient_complete_empty + cfc_old_complete_empty) + (cfc_old_complete_empty + cfc_old_complete_empty))))))))
  15. 0015specialize cf_convergent_matrix_empty_exists (s)
  16. 0016apply cf_convergent_matrix_empty_exists
  17. 0017cases hz
  18. 0018cases hz_witness
  19. 0019exists x
  20. 0020exists x1
  21. 0021exists 1
  22. 0022exists 0
  23. 0023exists 0
  24. 0024exists 1
  25. 0025specialize cf_convergent_matrix_length_transport (s)
  26. 0026specialize cf_convergent_matrix_length_transport (x)
  27. 0027specialize cf_convergent_matrix_length_transport (x1)
  28. 0028specialize cf_convergent_matrix_length_transport (0)
  29. 0029specialize cf_convergent_matrix_length_transport (k)
  30. 0030specialize cf_convergent_matrix_length_transport (1)
  31. 0031specialize cf_convergent_matrix_length_transport (0)
  32. 0032specialize cf_convergent_matrix_length_transport (0)
  33. 0033specialize cf_convergent_matrix_length_transport (1)
  34. 0034apply cf_convergent_matrix_length_transport
  35. 0035symm
  36. 0036exact hkzero
  37. 0037exact hz_witness_witness
  38. 0038intro k
  39. 0039intro a
  40. 0040intro b
  41. 0041intro s
  42. 0042intro h
  43. 0043intro e
  44. 0044intro ht
  45. 0045intro hk
  46. 0046have hkcase : k = 0 \/ exists i. k = S i
  47. 0047specialize zero_or_succ (k)
  48. 0048apply zero_or_succ
  49. 0049cases hkcase
  50. 0050have hz : exists H E. exists cfc_tail_complete_empty. ((exists cfc_state_complete_emptyinitial. ((exists cfc_left_complete_emptyinitialcode cfc_right_complete_emptyinitialcode cfc_matrix_complete_emptyinitialcode. ((cfc_left_complete_emptyinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_complete_emptyinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_complete_emptyinitialcode = ((cfc_left_complete_emptyinitialcode) + (cfc_right_complete_emptyinitialcode)) * S ((cfc_left_complete_emptyinitialcode) + (cfc_right_complete_emptyinitialcode)) + ((cfc_right_complete_emptyinitialcode) + (cfc_right_complete_emptyinitialcode))) /\ ((cfc_state_complete_emptyinitial) = ((cfc_tail_complete_empty) + (cfc_matrix_complete_emptyinitialcode)) * S ((cfc_tail_complete_empty) + (cfc_matrix_complete_emptyinitialcode)) + ((cfc_matrix_complete_emptyinitialcode) + (cfc_matrix_complete_emptyinitialcode))))))) /\ (((exists ff_h_complete_emptyinitialentry. ff_h_complete_emptyinitialentry + S (cfc_state_complete_emptyinitial) = S ((S (0)) * E)) /\ exists ff_q_complete_emptyinitialentry. H = ff_q_complete_emptyinitialentry * S ((S (0)) * E) + (cfc_state_complete_emptyinitial))))) /\ ((exists cfc_state_complete_emptyterminal. ((exists cfc_left_complete_emptyterminalcode cfc_right_complete_emptyterminalcode cfc_matrix_complete_emptyterminalcode. ((cfc_left_complete_emptyterminalcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_complete_emptyterminalcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_complete_emptyterminalcode = ((cfc_left_complete_emptyterminalcode) + (cfc_right_complete_emptyterminalcode)) * S ((cfc_left_complete_emptyterminalcode) + (cfc_right_complete_emptyterminalcode)) + ((cfc_right_complete_emptyterminalcode) + (cfc_right_complete_emptyterminalcode))) /\ ((cfc_state_complete_emptyterminal) = ((s) + (cfc_matrix_complete_emptyterminalcode)) * S ((s) + (cfc_matrix_complete_emptyterminalcode)) + ((cfc_matrix_complete_emptyterminalcode) + (cfc_matrix_complete_emptyterminalcode))))))) /\ (((exists ff_h_complete_emptyterminalentry. ff_h_complete_emptyterminalentry + S (cfc_state_complete_emptyterminal) = S ((S (0)) * E)) /\ exists ff_q_complete_emptyterminalentry. H = ff_q_complete_emptyterminalentry * S ((S (0)) * E) + (cfc_state_complete_emptyterminal))))) /\ (forall cfc_index_complete_empty. (exists cfba_gap_complete_emptybound. cfba_gap_complete_emptybound + S (cfc_index_complete_empty) = (0)) -> exists cfc_old_complete_empty cfc_a_complete_empty cfc_b_complete_empty cfc_c_complete_empty cfc_d_complete_empty cfc_new_complete_empty cfc_quotient_complete_empty. ((exists cfc_state_complete_emptyprevious. ((exists cfc_left_complete_emptypreviouscode cfc_right_complete_emptypreviouscode cfc_matrix_complete_emptypreviouscode. ((cfc_left_complete_emptypreviouscode = ((cfc_a_complete_empty) + (cfc_b_complete_empty)) * S ((cfc_a_complete_empty) + (cfc_b_complete_empty)) + ((cfc_b_complete_empty) + (cfc_b_complete_empty))) /\ ((cfc_right_complete_emptypreviouscode = ((cfc_c_complete_empty) + (cfc_d_complete_empty)) * S ((cfc_c_complete_empty) + (cfc_d_complete_empty)) + ((cfc_d_complete_empty) + (cfc_d_complete_empty))) /\ ((cfc_matrix_complete_emptypreviouscode = ((cfc_left_complete_emptypreviouscode) + (cfc_right_complete_emptypreviouscode)) * S ((cfc_left_complete_emptypreviouscode) + (cfc_right_complete_emptypreviouscode)) + ((cfc_right_complete_emptypreviouscode) + (cfc_right_complete_emptypreviouscode))) /\ ((cfc_state_complete_emptyprevious) = ((cfc_old_complete_empty) + (cfc_matrix_complete_emptypreviouscode)) * S ((cfc_old_complete_empty) + (cfc_matrix_complete_emptypreviouscode)) + ((cfc_matrix_complete_emptypreviouscode) + (cfc_matrix_complete_emptypreviouscode))))))) /\ (((exists ff_h_complete_emptypreviousentry. ff_h_complete_emptypreviousentry + S (cfc_state_complete_emptyprevious) = S ((S (cfc_index_complete_empty)) * E)) /\ exists ff_q_complete_emptypreviousentry. H = ff_q_complete_emptypreviousentry * S ((S (cfc_index_complete_empty)) * E) + (cfc_state_complete_emptyprevious))))) /\ ((exists cfc_state_complete_emptyfollowing. ((exists cfc_left_complete_emptyfollowingcode cfc_right_complete_emptyfollowingcode cfc_matrix_complete_emptyfollowingcode. ((cfc_left_complete_emptyfollowingcode = (((cfc_quotient_complete_empty * cfc_a_complete_empty + cfc_c_complete_empty)) + ((cfc_quotient_complete_empty * cfc_b_complete_empty + cfc_d_complete_empty))) * S (((cfc_quotient_complete_empty * cfc_a_complete_empty + cfc_c_complete_empty)) + ((cfc_quotient_complete_empty * cfc_b_complete_empty + cfc_d_complete_empty))) + (((cfc_quotient_complete_empty * cfc_b_complete_empty + cfc_d_complete_empty)) + ((cfc_quotient_complete_empty * cfc_b_complete_empty + cfc_d_complete_empty)))) /\ ((cfc_right_complete_emptyfollowingcode = ((cfc_a_complete_empty) + (cfc_b_complete_empty)) * S ((cfc_a_complete_empty) + (cfc_b_complete_empty)) + ((cfc_b_complete_empty) + (cfc_b_complete_empty))) /\ ((cfc_matrix_complete_emptyfollowingcode = ((cfc_left_complete_emptyfollowingcode) + (cfc_right_complete_emptyfollowingcode)) * S ((cfc_left_complete_emptyfollowingcode) + (cfc_right_complete_emptyfollowingcode)) + ((cfc_right_complete_emptyfollowingcode) + (cfc_right_complete_emptyfollowingcode))) /\ ((cfc_state_complete_emptyfollowing) = ((cfc_new_complete_empty) + (cfc_matrix_complete_emptyfollowingcode)) * S ((cfc_new_complete_empty) + (cfc_matrix_complete_emptyfollowingcode)) + ((cfc_matrix_complete_emptyfollowingcode) + (cfc_matrix_complete_emptyfollowingcode))))))) /\ (((exists ff_h_complete_emptyfollowingentry. ff_h_complete_emptyfollowingentry + S (cfc_state_complete_emptyfollowing) = S ((S (S cfc_index_complete_empty)) * E)) /\ exists ff_q_complete_emptyfollowingentry. H = ff_q_complete_emptyfollowingentry * S ((S (S cfc_index_complete_empty)) * E) + (cfc_state_complete_emptyfollowing))))) /\ (cfc_new_complete_empty = S ((cfc_quotient_complete_empty + cfc_old_complete_empty) * S (cfc_quotient_complete_empty + cfc_old_complete_empty) + (cfc_old_complete_empty + cfc_old_complete_empty))))))))
  51. 0051specialize cf_convergent_matrix_empty_exists (s)
  52. 0052apply cf_convergent_matrix_empty_exists
  53. 0053cases hz
  54. 0054cases hz_witness
  55. 0055exists x
  56. 0056exists x1
  57. 0057exists 1
  58. 0058exists 0
  59. 0059exists 0
  60. 0060exists 1
  61. 0061specialize cf_convergent_matrix_length_transport (s)
  62. 0062specialize cf_convergent_matrix_length_transport (x)
  63. 0063specialize cf_convergent_matrix_length_transport (x1)
  64. 0064specialize cf_convergent_matrix_length_transport (0)
  65. 0065specialize cf_convergent_matrix_length_transport (k)
  66. 0066specialize cf_convergent_matrix_length_transport (1)
  67. 0067specialize cf_convergent_matrix_length_transport (0)
  68. 0068specialize cf_convergent_matrix_length_transport (0)
  69. 0069specialize cf_convergent_matrix_length_transport (1)
  70. 0070apply cf_convergent_matrix_length_transport
  71. 0071symm
  72. 0072exact hkcase_left
  73. 0073exact hz_witness_witness
  74. 0074cases hkcase_right
  75. 0075have hp : exists q r t. ((a = b * q + r) /\ ((exists cfba_gap_complete_remainder. cfba_gap_complete_remainder + S (r) = (b)) /\ ((s = S ((q + t) * S (q + t) + (t + t))) /\ (exists cf_gcd_complete_predecessor. ((((exists ff_h_cf_complete_predecessor_initial_state. ff_h_cf_complete_predecessor_initial_state + S (((cf_gcd_complete_predecessor) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_complete_predecessor) + (((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_complete_predecessor_initial_state. h = ff_q_cf_complete_predecessor_initial_state * S ((S (0)) * e) + (((cf_gcd_complete_predecessor) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_complete_predecessor) + (((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_complete_predecessor_terminal_state. ff_h_cf_complete_predecessor_terminal_state + S (((b) + (((r) + (t)) * S ((r) + (t)) + ((t) + (t)))) * S ((b) + (((r) + (t)) * S ((r) + (t)) + ((t) + (t)))) + ((((r) + (t)) * S ((r) + (t)) + ((t) + (t))) + (((r) + (t)) * S ((r) + (t)) + ((t) + (t))))) = S ((S (L)) * e)) /\ exists ff_q_cf_complete_predecessor_terminal_state. h = ff_q_cf_complete_predecessor_terminal_state * S ((S (L)) * e) + (((b) + (((r) + (t)) * S ((r) + (t)) + ((t) + (t)))) * S ((b) + (((r) + (t)) * S ((r) + (t)) + ((t) + (t)))) + ((((r) + (t)) * S ((r) + (t)) + ((t) + (t))) + (((r) + (t)) * S ((r) + (t)) + ((t) + (t))))))) /\ forall cf_index_complete_predecessor. (exists ff_lt_cf_complete_predecessor_index. ff_lt_cf_complete_predecessor_index + S cf_index_complete_predecessor = L) -> exists cf_old_a_complete_predecessor cf_old_b_complete_predecessor cf_tail_complete_predecessor cf_new_a_complete_predecessor cf_new_b_complete_predecessor cf_head_complete_predecessor cf_quotient_complete_predecessor. ((((exists ff_h_cf_complete_predecessor_previous_state. ff_h_cf_complete_predecessor_previous_state + S (((cf_old_a_complete_predecessor) + (((cf_old_b_complete_predecessor) + (cf_tail_complete_predecessor)) * S ((cf_old_b_complete_predecessor) + (cf_tail_complete_predecessor)) + ((cf_tail_complete_predecessor) + (cf_tail_complete_predecessor)))) * S ((cf_old_a_complete_predecessor) + (((cf_old_b_complete_predecessor) + (cf_tail_complete_predecessor)) * S ((cf_old_b_complete_predecessor) + (cf_tail_complete_predecessor)) + ((cf_tail_complete_predecessor) + (cf_tail_complete_predecessor)))) + ((((cf_old_b_complete_predecessor) + (cf_tail_complete_predecessor)) * S ((cf_old_b_complete_predecessor) + (cf_tail_complete_predecessor)) + ((cf_tail_complete_predecessor) + (cf_tail_complete_predecessor))) + (((cf_old_b_complete_predecessor) + (cf_tail_complete_predecessor)) * S ((cf_old_b_complete_predecessor) + (cf_tail_complete_predecessor)) + ((cf_tail_complete_predecessor) + (cf_tail_complete_predecessor))))) = S ((S (cf_index_complete_predecessor)) * e)) /\ exists ff_q_cf_complete_predecessor_previous_state. h = ff_q_cf_complete_predecessor_previous_state * S ((S (cf_index_complete_predecessor)) * e) + (((cf_old_a_complete_predecessor) + (((cf_old_b_complete_predecessor) + (cf_tail_complete_predecessor)) * S ((cf_old_b_complete_predecessor) + (cf_tail_complete_predecessor)) + ((cf_tail_complete_predecessor) + (cf_tail_complete_predecessor)))) * S ((cf_old_a_complete_predecessor) + (((cf_old_b_complete_predecessor) + (cf_tail_complete_predecessor)) * S ((cf_old_b_complete_predecessor) + (cf_tail_complete_predecessor)) + ((cf_tail_complete_predecessor) + (cf_tail_complete_predecessor)))) + ((((cf_old_b_complete_predecessor) + (cf_tail_complete_predecessor)) * S ((cf_old_b_complete_predecessor) + (cf_tail_complete_predecessor)) + ((cf_tail_complete_predecessor) + (cf_tail_complete_predecessor))) + (((cf_old_b_complete_predecessor) + (cf_tail_complete_predecessor)) * S ((cf_old_b_complete_predecessor) + (cf_tail_complete_predecessor)) + ((cf_tail_complete_predecessor) + (cf_tail_complete_predecessor))))))) /\ ((((exists ff_h_cf_complete_predecessor_following_state. ff_h_cf_complete_predecessor_following_state + S (((cf_new_a_complete_predecessor) + (((cf_new_b_complete_predecessor) + (cf_head_complete_predecessor)) * S ((cf_new_b_complete_predecessor) + (cf_head_complete_predecessor)) + ((cf_head_complete_predecessor) + (cf_head_complete_predecessor)))) * S ((cf_new_a_complete_predecessor) + (((cf_new_b_complete_predecessor) + (cf_head_complete_predecessor)) * S ((cf_new_b_complete_predecessor) + (cf_head_complete_predecessor)) + ((cf_head_complete_predecessor) + (cf_head_complete_predecessor)))) + ((((cf_new_b_complete_predecessor) + (cf_head_complete_predecessor)) * S ((cf_new_b_complete_predecessor) + (cf_head_complete_predecessor)) + ((cf_head_complete_predecessor) + (cf_head_complete_predecessor))) + (((cf_new_b_complete_predecessor) + (cf_head_complete_predecessor)) * S ((cf_new_b_complete_predecessor) + (cf_head_complete_predecessor)) + ((cf_head_complete_predecessor) + (cf_head_complete_predecessor))))) = S ((S (S cf_index_complete_predecessor)) * e)) /\ exists ff_q_cf_complete_predecessor_following_state. h = ff_q_cf_complete_predecessor_following_state * S ((S (S cf_index_complete_predecessor)) * e) + (((cf_new_a_complete_predecessor) + (((cf_new_b_complete_predecessor) + (cf_head_complete_predecessor)) * S ((cf_new_b_complete_predecessor) + (cf_head_complete_predecessor)) + ((cf_head_complete_predecessor) + (cf_head_complete_predecessor)))) * S ((cf_new_a_complete_predecessor) + (((cf_new_b_complete_predecessor) + (cf_head_complete_predecessor)) * S ((cf_new_b_complete_predecessor) + (cf_head_complete_predecessor)) + ((cf_head_complete_predecessor) + (cf_head_complete_predecessor)))) + ((((cf_new_b_complete_predecessor) + (cf_head_complete_predecessor)) * S ((cf_new_b_complete_predecessor) + (cf_head_complete_predecessor)) + ((cf_head_complete_predecessor) + (cf_head_complete_predecessor))) + (((cf_new_b_complete_predecessor) + (cf_head_complete_predecessor)) * S ((cf_new_b_complete_predecessor) + (cf_head_complete_predecessor)) + ((cf_head_complete_predecessor) + (cf_head_complete_predecessor))))))) /\ (cf_new_b_complete_predecessor = cf_old_a_complete_predecessor /\ (cf_new_a_complete_predecessor = cf_new_b_complete_predecessor * cf_quotient_complete_predecessor + cf_old_b_complete_predecessor /\ ((exists ff_lt_cf_complete_predecessor_remainder. ff_lt_cf_complete_predecessor_remainder + S cf_old_b_complete_predecessor = cf_new_b_complete_predecessor) /\ (cf_head_complete_predecessor = S ((cf_quotient_complete_predecessor + cf_tail_complete_predecessor) * S (cf_quotient_complete_predecessor + cf_tail_complete_predecessor) + (cf_tail_complete_predecessor + cf_tail_complete_predecessor))))))))))))))
  76. 0076specialize cf_convergent_old_history_successor_elimination (a)
  77. 0077specialize cf_convergent_old_history_successor_elimination (b)
  78. 0078specialize cf_convergent_old_history_successor_elimination (s)
  79. 0079specialize cf_convergent_old_history_successor_elimination (h)
  80. 0080specialize cf_convergent_old_history_successor_elimination (e)
  81. 0081specialize cf_convergent_old_history_successor_elimination (L)
  82. 0082apply cf_convergent_old_history_successor_elimination
  83. 0083exact ht
  84. 0084cases hp
  85. 0085cases hp_witness
  86. 0086cases hp_witness_witness
  87. 0087cases hp_witness_witness_witness
  88. 0088cases hp_witness_witness_witness_right
  89. 0089cases hp_witness_witness_witness_right_right
  90. 0090have hc : exists cfc_h_complete_child cfc_e_complete_child cfc_u_complete_child cfc_U_complete_child cfc_v_complete_child cfc_V_complete_child. exists cfc_tail_complete_childbody. ((exists cfc_state_complete_childbodyinitial. ((exists cfc_left_complete_childbodyinitialcode cfc_right_complete_childbodyinitialcode cfc_matrix_complete_childbodyinitialcode. ((cfc_left_complete_childbodyinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_complete_childbodyinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_complete_childbodyinitialcode = ((cfc_left_complete_childbodyinitialcode) + (cfc_right_complete_childbodyinitialcode)) * S ((cfc_left_complete_childbodyinitialcode) + (cfc_right_complete_childbodyinitialcode)) + ((cfc_right_complete_childbodyinitialcode) + (cfc_right_complete_childbodyinitialcode))) /\ ((cfc_state_complete_childbodyinitial) = ((cfc_tail_complete_childbody) + (cfc_matrix_complete_childbodyinitialcode)) * S ((cfc_tail_complete_childbody) + (cfc_matrix_complete_childbodyinitialcode)) + ((cfc_matrix_complete_childbodyinitialcode) + (cfc_matrix_complete_childbodyinitialcode))))))) /\ (((exists ff_h_complete_childbodyinitialentry. ff_h_complete_childbodyinitialentry + S (cfc_state_complete_childbodyinitial) = S ((S (0)) * cfc_e_complete_child)) /\ exists ff_q_complete_childbodyinitialentry. cfc_h_complete_child = ff_q_complete_childbodyinitialentry * S ((S (0)) * cfc_e_complete_child) + (cfc_state_complete_childbodyinitial))))) /\ ((exists cfc_state_complete_childbodyterminal. ((exists cfc_left_complete_childbodyterminalcode cfc_right_complete_childbodyterminalcode cfc_matrix_complete_childbodyterminalcode. ((cfc_left_complete_childbodyterminalcode = ((cfc_u_complete_child) + (cfc_U_complete_child)) * S ((cfc_u_complete_child) + (cfc_U_complete_child)) + ((cfc_U_complete_child) + (cfc_U_complete_child))) /\ ((cfc_right_complete_childbodyterminalcode = ((cfc_v_complete_child) + (cfc_V_complete_child)) * S ((cfc_v_complete_child) + (cfc_V_complete_child)) + ((cfc_V_complete_child) + (cfc_V_complete_child))) /\ ((cfc_matrix_complete_childbodyterminalcode = ((cfc_left_complete_childbodyterminalcode) + (cfc_right_complete_childbodyterminalcode)) * S ((cfc_left_complete_childbodyterminalcode) + (cfc_right_complete_childbodyterminalcode)) + ((cfc_right_complete_childbodyterminalcode) + (cfc_right_complete_childbodyterminalcode))) /\ ((cfc_state_complete_childbodyterminal) = ((x3) + (cfc_matrix_complete_childbodyterminalcode)) * S ((x3) + (cfc_matrix_complete_childbodyterminalcode)) + ((cfc_matrix_complete_childbodyterminalcode) + (cfc_matrix_complete_childbodyterminalcode))))))) /\ (((exists ff_h_complete_childbodyterminalentry. ff_h_complete_childbodyterminalentry + S (cfc_state_complete_childbodyterminal) = S ((S (x)) * cfc_e_complete_child)) /\ exists ff_q_complete_childbodyterminalentry. cfc_h_complete_child = ff_q_complete_childbodyterminalentry * S ((S (x)) * cfc_e_complete_child) + (cfc_state_complete_childbodyterminal))))) /\ (forall cfc_index_complete_childbody. (exists cfba_gap_complete_childbodybound. cfba_gap_complete_childbodybound + S (cfc_index_complete_childbody) = (x)) -> exists cfc_old_complete_childbody cfc_a_complete_childbody cfc_b_complete_childbody cfc_c_complete_childbody cfc_d_complete_childbody cfc_new_complete_childbody cfc_quotient_complete_childbody. ((exists cfc_state_complete_childbodyprevious. ((exists cfc_left_complete_childbodypreviouscode cfc_right_complete_childbodypreviouscode cfc_matrix_complete_childbodypreviouscode. ((cfc_left_complete_childbodypreviouscode = ((cfc_a_complete_childbody) + (cfc_b_complete_childbody)) * S ((cfc_a_complete_childbody) + (cfc_b_complete_childbody)) + ((cfc_b_complete_childbody) + (cfc_b_complete_childbody))) /\ ((cfc_right_complete_childbodypreviouscode = ((cfc_c_complete_childbody) + (cfc_d_complete_childbody)) * S ((cfc_c_complete_childbody) + (cfc_d_complete_childbody)) + ((cfc_d_complete_childbody) + (cfc_d_complete_childbody))) /\ ((cfc_matrix_complete_childbodypreviouscode = ((cfc_left_complete_childbodypreviouscode) + (cfc_right_complete_childbodypreviouscode)) * S ((cfc_left_complete_childbodypreviouscode) + (cfc_right_complete_childbodypreviouscode)) + ((cfc_right_complete_childbodypreviouscode) + (cfc_right_complete_childbodypreviouscode))) /\ ((cfc_state_complete_childbodyprevious) = ((cfc_old_complete_childbody) + (cfc_matrix_complete_childbodypreviouscode)) * S ((cfc_old_complete_childbody) + (cfc_matrix_complete_childbodypreviouscode)) + ((cfc_matrix_complete_childbodypreviouscode) + (cfc_matrix_complete_childbodypreviouscode))))))) /\ (((exists ff_h_complete_childbodypreviousentry. ff_h_complete_childbodypreviousentry + S (cfc_state_complete_childbodyprevious) = S ((S (cfc_index_complete_childbody)) * cfc_e_complete_child)) /\ exists ff_q_complete_childbodypreviousentry. cfc_h_complete_child = ff_q_complete_childbodypreviousentry * S ((S (cfc_index_complete_childbody)) * cfc_e_complete_child) + (cfc_state_complete_childbodyprevious))))) /\ ((exists cfc_state_complete_childbodyfollowing. ((exists cfc_left_complete_childbodyfollowingcode cfc_right_complete_childbodyfollowingcode cfc_matrix_complete_childbodyfollowingcode. ((cfc_left_complete_childbodyfollowingcode = (((cfc_quotient_complete_childbody * cfc_a_complete_childbody + cfc_c_complete_childbody)) + ((cfc_quotient_complete_childbody * cfc_b_complete_childbody + cfc_d_complete_childbody))) * S (((cfc_quotient_complete_childbody * cfc_a_complete_childbody + cfc_c_complete_childbody)) + ((cfc_quotient_complete_childbody * cfc_b_complete_childbody + cfc_d_complete_childbody))) + (((cfc_quotient_complete_childbody * cfc_b_complete_childbody + cfc_d_complete_childbody)) + ((cfc_quotient_complete_childbody * cfc_b_complete_childbody + cfc_d_complete_childbody)))) /\ ((cfc_right_complete_childbodyfollowingcode = ((cfc_a_complete_childbody) + (cfc_b_complete_childbody)) * S ((cfc_a_complete_childbody) + (cfc_b_complete_childbody)) + ((cfc_b_complete_childbody) + (cfc_b_complete_childbody))) /\ ((cfc_matrix_complete_childbodyfollowingcode = ((cfc_left_complete_childbodyfollowingcode) + (cfc_right_complete_childbodyfollowingcode)) * S ((cfc_left_complete_childbodyfollowingcode) + (cfc_right_complete_childbodyfollowingcode)) + ((cfc_right_complete_childbodyfollowingcode) + (cfc_right_complete_childbodyfollowingcode))) /\ ((cfc_state_complete_childbodyfollowing) = ((cfc_new_complete_childbody) + (cfc_matrix_complete_childbodyfollowingcode)) * S ((cfc_new_complete_childbody) + (cfc_matrix_complete_childbodyfollowingcode)) + ((cfc_matrix_complete_childbodyfollowingcode) + (cfc_matrix_complete_childbodyfollowingcode))))))) /\ (((exists ff_h_complete_childbodyfollowingentry. ff_h_complete_childbodyfollowingentry + S (cfc_state_complete_childbodyfollowing) = S ((S (S cfc_index_complete_childbody)) * cfc_e_complete_child)) /\ exists ff_q_complete_childbodyfollowingentry. cfc_h_complete_child = ff_q_complete_childbodyfollowingentry * S ((S (S cfc_index_complete_childbody)) * cfc_e_complete_child) + (cfc_state_complete_childbodyfollowing))))) /\ (cfc_new_complete_childbody = S ((cfc_quotient_complete_childbody + cfc_old_complete_childbody) * S (cfc_quotient_complete_childbody + cfc_old_complete_childbody) + (cfc_old_complete_childbody + cfc_old_complete_childbody))))))))
  91. 0091specialize IH (x)
  92. 0092specialize IH (b)
  93. 0093specialize IH (x2)
  94. 0094specialize IH (x3)
  95. 0095specialize IH (h)
  96. 0096specialize IH (e)
  97. 0097apply IH
  98. 0098exact hp_witness_witness_witness_right_right_right
  99. 0099specialize le_of_succ_le_succ (x)
  100. 0100specialize le_of_succ_le_succ (L)
  101. 0101apply le_of_succ_le_succ
  102. 0102rewrite <- hkcase_right_witness
  103. 0103exact hk
  104. 0104cases hc
  105. 0105cases hc_witness
  106. 0106cases hc_witness_witness
  107. 0107cases hc_witness_witness_witness
  108. 0108cases hc_witness_witness_witness_witness
  109. 0109cases hc_witness_witness_witness_witness_witness
  110. 0110have hext : exists H E. exists cfc_tail_complete_extension. ((exists cfc_state_complete_extensioninitial. ((exists cfc_left_complete_extensioninitialcode cfc_right_complete_extensioninitialcode cfc_matrix_complete_extensioninitialcode. ((cfc_left_complete_extensioninitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_complete_extensioninitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_complete_extensioninitialcode = ((cfc_left_complete_extensioninitialcode) + (cfc_right_complete_extensioninitialcode)) * S ((cfc_left_complete_extensioninitialcode) + (cfc_right_complete_extensioninitialcode)) + ((cfc_right_complete_extensioninitialcode) + (cfc_right_complete_extensioninitialcode))) /\ ((cfc_state_complete_extensioninitial) = ((cfc_tail_complete_extension) + (cfc_matrix_complete_extensioninitialcode)) * S ((cfc_tail_complete_extension) + (cfc_matrix_complete_extensioninitialcode)) + ((cfc_matrix_complete_extensioninitialcode) + (cfc_matrix_complete_extensioninitialcode))))))) /\ (((exists ff_h_complete_extensioninitialentry. ff_h_complete_extensioninitialentry + S (cfc_state_complete_extensioninitial) = S ((S (0)) * E)) /\ exists ff_q_complete_extensioninitialentry. H = ff_q_complete_extensioninitialentry * S ((S (0)) * E) + (cfc_state_complete_extensioninitial))))) /\ ((exists cfc_state_complete_extensionterminal. ((exists cfc_left_complete_extensionterminalcode cfc_right_complete_extensionterminalcode cfc_matrix_complete_extensionterminalcode. ((cfc_left_complete_extensionterminalcode = (((x1 * x6 + x8)) + ((x1 * x7 + x9))) * S (((x1 * x6 + x8)) + ((x1 * x7 + x9))) + (((x1 * x7 + x9)) + ((x1 * x7 + x9)))) /\ ((cfc_right_complete_extensionterminalcode = ((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))) /\ ((cfc_matrix_complete_extensionterminalcode = ((cfc_left_complete_extensionterminalcode) + (cfc_right_complete_extensionterminalcode)) * S ((cfc_left_complete_extensionterminalcode) + (cfc_right_complete_extensionterminalcode)) + ((cfc_right_complete_extensionterminalcode) + (cfc_right_complete_extensionterminalcode))) /\ ((cfc_state_complete_extensionterminal) = ((s) + (cfc_matrix_complete_extensionterminalcode)) * S ((s) + (cfc_matrix_complete_extensionterminalcode)) + ((cfc_matrix_complete_extensionterminalcode) + (cfc_matrix_complete_extensionterminalcode))))))) /\ (((exists ff_h_complete_extensionterminalentry. ff_h_complete_extensionterminalentry + S (cfc_state_complete_extensionterminal) = S ((S (S x)) * E)) /\ exists ff_q_complete_extensionterminalentry. H = ff_q_complete_extensionterminalentry * S ((S (S x)) * E) + (cfc_state_complete_extensionterminal))))) /\ (forall cfc_index_complete_extension. (exists cfba_gap_complete_extensionbound. cfba_gap_complete_extensionbound + S (cfc_index_complete_extension) = (S x)) -> exists cfc_old_complete_extension cfc_a_complete_extension cfc_b_complete_extension cfc_c_complete_extension cfc_d_complete_extension cfc_new_complete_extension cfc_quotient_complete_extension. ((exists cfc_state_complete_extensionprevious. ((exists cfc_left_complete_extensionpreviouscode cfc_right_complete_extensionpreviouscode cfc_matrix_complete_extensionpreviouscode. ((cfc_left_complete_extensionpreviouscode = ((cfc_a_complete_extension) + (cfc_b_complete_extension)) * S ((cfc_a_complete_extension) + (cfc_b_complete_extension)) + ((cfc_b_complete_extension) + (cfc_b_complete_extension))) /\ ((cfc_right_complete_extensionpreviouscode = ((cfc_c_complete_extension) + (cfc_d_complete_extension)) * S ((cfc_c_complete_extension) + (cfc_d_complete_extension)) + ((cfc_d_complete_extension) + (cfc_d_complete_extension))) /\ ((cfc_matrix_complete_extensionpreviouscode = ((cfc_left_complete_extensionpreviouscode) + (cfc_right_complete_extensionpreviouscode)) * S ((cfc_left_complete_extensionpreviouscode) + (cfc_right_complete_extensionpreviouscode)) + ((cfc_right_complete_extensionpreviouscode) + (cfc_right_complete_extensionpreviouscode))) /\ ((cfc_state_complete_extensionprevious) = ((cfc_old_complete_extension) + (cfc_matrix_complete_extensionpreviouscode)) * S ((cfc_old_complete_extension) + (cfc_matrix_complete_extensionpreviouscode)) + ((cfc_matrix_complete_extensionpreviouscode) + (cfc_matrix_complete_extensionpreviouscode))))))) /\ (((exists ff_h_complete_extensionpreviousentry. ff_h_complete_extensionpreviousentry + S (cfc_state_complete_extensionprevious) = S ((S (cfc_index_complete_extension)) * E)) /\ exists ff_q_complete_extensionpreviousentry. H = ff_q_complete_extensionpreviousentry * S ((S (cfc_index_complete_extension)) * E) + (cfc_state_complete_extensionprevious))))) /\ ((exists cfc_state_complete_extensionfollowing. ((exists cfc_left_complete_extensionfollowingcode cfc_right_complete_extensionfollowingcode cfc_matrix_complete_extensionfollowingcode. ((cfc_left_complete_extensionfollowingcode = (((cfc_quotient_complete_extension * cfc_a_complete_extension + cfc_c_complete_extension)) + ((cfc_quotient_complete_extension * cfc_b_complete_extension + cfc_d_complete_extension))) * S (((cfc_quotient_complete_extension * cfc_a_complete_extension + cfc_c_complete_extension)) + ((cfc_quotient_complete_extension * cfc_b_complete_extension + cfc_d_complete_extension))) + (((cfc_quotient_complete_extension * cfc_b_complete_extension + cfc_d_complete_extension)) + ((cfc_quotient_complete_extension * cfc_b_complete_extension + cfc_d_complete_extension)))) /\ ((cfc_right_complete_extensionfollowingcode = ((cfc_a_complete_extension) + (cfc_b_complete_extension)) * S ((cfc_a_complete_extension) + (cfc_b_complete_extension)) + ((cfc_b_complete_extension) + (cfc_b_complete_extension))) /\ ((cfc_matrix_complete_extensionfollowingcode = ((cfc_left_complete_extensionfollowingcode) + (cfc_right_complete_extensionfollowingcode)) * S ((cfc_left_complete_extensionfollowingcode) + (cfc_right_complete_extensionfollowingcode)) + ((cfc_right_complete_extensionfollowingcode) + (cfc_right_complete_extensionfollowingcode))) /\ ((cfc_state_complete_extensionfollowing) = ((cfc_new_complete_extension) + (cfc_matrix_complete_extensionfollowingcode)) * S ((cfc_new_complete_extension) + (cfc_matrix_complete_extensionfollowingcode)) + ((cfc_matrix_complete_extensionfollowingcode) + (cfc_matrix_complete_extensionfollowingcode))))))) /\ (((exists ff_h_complete_extensionfollowingentry. ff_h_complete_extensionfollowingentry + S (cfc_state_complete_extensionfollowing) = S ((S (S cfc_index_complete_extension)) * E)) /\ exists ff_q_complete_extensionfollowingentry. H = ff_q_complete_extensionfollowingentry * S ((S (S cfc_index_complete_extension)) * E) + (cfc_state_complete_extensionfollowing))))) /\ (cfc_new_complete_extension = S ((cfc_quotient_complete_extension + cfc_old_complete_extension) * S (cfc_quotient_complete_extension + cfc_old_complete_extension) + (cfc_old_complete_extension + cfc_old_complete_extension))))))))
  111. 0111specialize cf_convergent_matrix_prepend_exists (x3)
  112. 0112specialize cf_convergent_matrix_prepend_exists (x4)
  113. 0113specialize cf_convergent_matrix_prepend_exists (x5)
  114. 0114specialize cf_convergent_matrix_prepend_exists (x)
  115. 0115specialize cf_convergent_matrix_prepend_exists (x6)
  116. 0116specialize cf_convergent_matrix_prepend_exists (x7)
  117. 0117specialize cf_convergent_matrix_prepend_exists (x8)
  118. 0118specialize cf_convergent_matrix_prepend_exists (x9)
  119. 0119specialize cf_convergent_matrix_prepend_exists (x1)
  120. 0120specialize cf_convergent_matrix_prepend_exists (s)
  121. 0121apply cf_convergent_matrix_prepend_exists
  122. 0122exact hc_witness_witness_witness_witness_witness_witness
  123. 0123exact hp_witness_witness_witness_right_right_left
  124. 0124cases hext
  125. 0125cases hext_witness
  126. 0126exists x10
  127. 0127exists x11
  128. 0128exists x1 * x6 + x8
  129. 0129exists x1 * x7 + x9
  130. 0130exists x6
  131. 0131exists x7
  132. 0132specialize cf_convergent_matrix_length_transport (s)
  133. 0133specialize cf_convergent_matrix_length_transport (x10)
  134. 0134specialize cf_convergent_matrix_length_transport (x11)
  135. 0135specialize cf_convergent_matrix_length_transport (S x)
  136. 0136specialize cf_convergent_matrix_length_transport (k)
  137. 0137specialize cf_convergent_matrix_length_transport (x1 * x6 + x8)
  138. 0138specialize cf_convergent_matrix_length_transport (x1 * x7 + x9)
  139. 0139specialize cf_convergent_matrix_length_transport (x6)
  140. 0140specialize cf_convergent_matrix_length_transport (x7)
  141. 0141apply cf_convergent_matrix_length_transport
  142. 0142symm
  143. 0143exact hkcase_right_witness
  144. 0144exact hext_witness_witness