BA004F

cf_convergent_second_column_is_previous_prefix

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

The second matrix column is proved to be the actual previous quotient prefix of the same original list, not an arbitrary auxiliary vector chosen to make the determinant or approximation proof work.

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 s h e u U v V. (exists cfc_tail_previous_column_source. ((exists cfc_state_previous_column_sourceinitial. ((exists cfc_left_previous_column_sourceinitialcode cfc_right_previous_column_sourceinitialcode cfc_matrix_previous_column_sourceinitialcode. ((cfc_left_previous_column_sourceinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_previous_column_sourceinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_previous_column_sourceinitialcode = ((cfc_left_previous_column_sourceinitialcode) + (cfc_right_previous_column_sourceinitialcode)) * S ((cfc_left_previous_column_sourceinitialcode) + (cfc_right_previous_column_sourceinitialcode)) + ((cfc_right_previous_column_sourceinitialcode) + (cfc_right_previous_column_sourceinitialcode))) /\ ((cfc_state_previous_column_sourceinitial) = ((cfc_tail_previous_column_source) + (cfc_matrix_previous_column_sourceinitialcode)) * S ((cfc_tail_previous_column_source) + (cfc_matrix_previous_column_sourceinitialcode)) + ((cfc_matrix_previous_column_sourceinitialcode) + (cfc_matrix_previous_column_sourceinitialcode))))))) /\ (((exists ff_h_previous_column_sourceinitialentry. ff_h_previous_column_sourceinitialentry + S (cfc_state_previous_column_sourceinitial) = S ((S (0)) * e)) /\ exists ff_q_previous_column_sourceinitialentry. h = ff_q_previous_column_sourceinitialentry * S ((S (0)) * e) + (cfc_state_previous_column_sourceinitial))))) /\ ((exists cfc_state_previous_column_sourceterminal. ((exists cfc_left_previous_column_sourceterminalcode cfc_right_previous_column_sourceterminalcode cfc_matrix_previous_column_sourceterminalcode. ((cfc_left_previous_column_sourceterminalcode = ((u) + (U)) * S ((u) + (U)) + ((U) + (U))) /\ ((cfc_right_previous_column_sourceterminalcode = ((v) + (V)) * S ((v) + (V)) + ((V) + (V))) /\ ((cfc_matrix_previous_column_sourceterminalcode = ((cfc_left_previous_column_sourceterminalcode) + (cfc_right_previous_column_sourceterminalcode)) * S ((cfc_left_previous_column_sourceterminalcode) + (cfc_right_previous_column_sourceterminalcode)) + ((cfc_right_previous_column_sourceterminalcode) + (cfc_right_previous_column_sourceterminalcode))) /\ ((cfc_state_previous_column_sourceterminal) = ((s) + (cfc_matrix_previous_column_sourceterminalcode)) * S ((s) + (cfc_matrix_previous_column_sourceterminalcode)) + ((cfc_matrix_previous_column_sourceterminalcode) + (cfc_matrix_previous_column_sourceterminalcode))))))) /\ (((exists ff_h_previous_column_sourceterminalentry. ff_h_previous_column_sourceterminalentry + S (cfc_state_previous_column_sourceterminal) = S ((S (S k)) * e)) /\ exists ff_q_previous_column_sourceterminalentry. h = ff_q_previous_column_sourceterminalentry * S ((S (S k)) * e) + (cfc_state_previous_column_sourceterminal))))) /\ (forall cfc_index_previous_column_source. (exists cfba_gap_previous_column_sourcebound. cfba_gap_previous_column_sourcebound + S (cfc_index_previous_column_source) = (S k)) -> exists cfc_old_previous_column_source cfc_a_previous_column_source cfc_b_previous_column_source cfc_c_previous_column_source cfc_d_previous_column_source cfc_new_previous_column_source cfc_quotient_previous_column_source. ((exists cfc_state_previous_column_sourceprevious. ((exists cfc_left_previous_column_sourcepreviouscode cfc_right_previous_column_sourcepreviouscode cfc_matrix_previous_column_sourcepreviouscode. ((cfc_left_previous_column_sourcepreviouscode = ((cfc_a_previous_column_source) + (cfc_b_previous_column_source)) * S ((cfc_a_previous_column_source) + (cfc_b_previous_column_source)) + ((cfc_b_previous_column_source) + (cfc_b_previous_column_source))) /\ ((cfc_right_previous_column_sourcepreviouscode = ((cfc_c_previous_column_source) + (cfc_d_previous_column_source)) * S ((cfc_c_previous_column_source) + (cfc_d_previous_column_source)) + ((cfc_d_previous_column_source) + (cfc_d_previous_column_source))) /\ ((cfc_matrix_previous_column_sourcepreviouscode = ((cfc_left_previous_column_sourcepreviouscode) + (cfc_right_previous_column_sourcepreviouscode)) * S ((cfc_left_previous_column_sourcepreviouscode) + (cfc_right_previous_column_sourcepreviouscode)) + ((cfc_right_previous_column_sourcepreviouscode) + (cfc_right_previous_column_sourcepreviouscode))) /\ ((cfc_state_previous_column_sourceprevious) = ((cfc_old_previous_column_source) + (cfc_matrix_previous_column_sourcepreviouscode)) * S ((cfc_old_previous_column_source) + (cfc_matrix_previous_column_sourcepreviouscode)) + ((cfc_matrix_previous_column_sourcepreviouscode) + (cfc_matrix_previous_column_sourcepreviouscode))))))) /\ (((exists ff_h_previous_column_sourcepreviousentry. ff_h_previous_column_sourcepreviousentry + S (cfc_state_previous_column_sourceprevious) = S ((S (cfc_index_previous_column_source)) * e)) /\ exists ff_q_previous_column_sourcepreviousentry. h = ff_q_previous_column_sourcepreviousentry * S ((S (cfc_index_previous_column_source)) * e) + (cfc_state_previous_column_sourceprevious))))) /\ ((exists cfc_state_previous_column_sourcefollowing. ((exists cfc_left_previous_column_sourcefollowingcode cfc_right_previous_column_sourcefollowingcode cfc_matrix_previous_column_sourcefollowingcode. ((cfc_left_previous_column_sourcefollowingcode = (((cfc_quotient_previous_column_source * cfc_a_previous_column_source + cfc_c_previous_column_source)) + ((cfc_quotient_previous_column_source * cfc_b_previous_column_source + cfc_d_previous_column_source))) * S (((cfc_quotient_previous_column_source * cfc_a_previous_column_source + cfc_c_previous_column_source)) + ((cfc_quotient_previous_column_source * cfc_b_previous_column_source + cfc_d_previous_column_source))) + (((cfc_quotient_previous_column_source * cfc_b_previous_column_source + cfc_d_previous_column_source)) + ((cfc_quotient_previous_column_source * cfc_b_previous_column_source + cfc_d_previous_column_source)))) /\ ((cfc_right_previous_column_sourcefollowingcode = ((cfc_a_previous_column_source) + (cfc_b_previous_column_source)) * S ((cfc_a_previous_column_source) + (cfc_b_previous_column_source)) + ((cfc_b_previous_column_source) + (cfc_b_previous_column_source))) /\ ((cfc_matrix_previous_column_sourcefollowingcode = ((cfc_left_previous_column_sourcefollowingcode) + (cfc_right_previous_column_sourcefollowingcode)) * S ((cfc_left_previous_column_sourcefollowingcode) + (cfc_right_previous_column_sourcefollowingcode)) + ((cfc_right_previous_column_sourcefollowingcode) + (cfc_right_previous_column_sourcefollowingcode))) /\ ((cfc_state_previous_column_sourcefollowing) = ((cfc_new_previous_column_source) + (cfc_matrix_previous_column_sourcefollowingcode)) * S ((cfc_new_previous_column_source) + (cfc_matrix_previous_column_sourcefollowingcode)) + ((cfc_matrix_previous_column_sourcefollowingcode) + (cfc_matrix_previous_column_sourcefollowingcode))))))) /\ (((exists ff_h_previous_column_sourcefollowingentry. ff_h_previous_column_sourcefollowingentry + S (cfc_state_previous_column_sourcefollowing) = S ((S (S cfc_index_previous_column_source)) * e)) /\ exists ff_q_previous_column_sourcefollowingentry. h = ff_q_previous_column_sourcefollowingentry * S ((S (S cfc_index_previous_column_source)) * e) + (cfc_state_previous_column_sourcefollowing))))) /\ (cfc_new_previous_column_source = S ((cfc_quotient_previous_column_source + cfc_old_previous_column_source) * S (cfc_quotient_previous_column_source + cfc_old_previous_column_source) + (cfc_old_previous_column_source + cfc_old_previous_column_source))))))))) -> (exists cfc_h_previous_column_result cfc_e_previous_column_result cfc_p_previous_column_result cfc_q_previous_column_result. exists cfc_tail_previous_column_resultbody. ((exists cfc_state_previous_column_resultbodyinitial. ((exists cfc_left_previous_column_resultbodyinitialcode cfc_right_previous_column_resultbodyinitialcode cfc_matrix_previous_column_resultbodyinitialcode. ((cfc_left_previous_column_resultbodyinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_previous_column_resultbodyinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_previous_column_resultbodyinitialcode = ((cfc_left_previous_column_resultbodyinitialcode) + (cfc_right_previous_column_resultbodyinitialcode)) * S ((cfc_left_previous_column_resultbodyinitialcode) + (cfc_right_previous_column_resultbodyinitialcode)) + ((cfc_right_previous_column_resultbodyinitialcode) + (cfc_right_previous_column_resultbodyinitialcode))) /\ ((cfc_state_previous_column_resultbodyinitial) = ((cfc_tail_previous_column_resultbody) + (cfc_matrix_previous_column_resultbodyinitialcode)) * S ((cfc_tail_previous_column_resultbody) + (cfc_matrix_previous_column_resultbodyinitialcode)) + ((cfc_matrix_previous_column_resultbodyinitialcode) + (cfc_matrix_previous_column_resultbodyinitialcode))))))) /\ (((exists ff_h_previous_column_resultbodyinitialentry. ff_h_previous_column_resultbodyinitialentry + S (cfc_state_previous_column_resultbodyinitial) = S ((S (0)) * cfc_e_previous_column_result)) /\ exists ff_q_previous_column_resultbodyinitialentry. cfc_h_previous_column_result = ff_q_previous_column_resultbodyinitialentry * S ((S (0)) * cfc_e_previous_column_result) + (cfc_state_previous_column_resultbodyinitial))))) /\ ((exists cfc_state_previous_column_resultbodyterminal. ((exists cfc_left_previous_column_resultbodyterminalcode cfc_right_previous_column_resultbodyterminalcode cfc_matrix_previous_column_resultbodyterminalcode. ((cfc_left_previous_column_resultbodyterminalcode = ((U) + (cfc_p_previous_column_result)) * S ((U) + (cfc_p_previous_column_result)) + ((cfc_p_previous_column_result) + (cfc_p_previous_column_result))) /\ ((cfc_right_previous_column_resultbodyterminalcode = ((V) + (cfc_q_previous_column_result)) * S ((V) + (cfc_q_previous_column_result)) + ((cfc_q_previous_column_result) + (cfc_q_previous_column_result))) /\ ((cfc_matrix_previous_column_resultbodyterminalcode = ((cfc_left_previous_column_resultbodyterminalcode) + (cfc_right_previous_column_resultbodyterminalcode)) * S ((cfc_left_previous_column_resultbodyterminalcode) + (cfc_right_previous_column_resultbodyterminalcode)) + ((cfc_right_previous_column_resultbodyterminalcode) + (cfc_right_previous_column_resultbodyterminalcode))) /\ ((cfc_state_previous_column_resultbodyterminal) = ((s) + (cfc_matrix_previous_column_resultbodyterminalcode)) * S ((s) + (cfc_matrix_previous_column_resultbodyterminalcode)) + ((cfc_matrix_previous_column_resultbodyterminalcode) + (cfc_matrix_previous_column_resultbodyterminalcode))))))) /\ (((exists ff_h_previous_column_resultbodyterminalentry. ff_h_previous_column_resultbodyterminalentry + S (cfc_state_previous_column_resultbodyterminal) = S ((S (k)) * cfc_e_previous_column_result)) /\ exists ff_q_previous_column_resultbodyterminalentry. cfc_h_previous_column_result = ff_q_previous_column_resultbodyterminalentry * S ((S (k)) * cfc_e_previous_column_result) + (cfc_state_previous_column_resultbodyterminal))))) /\ (forall cfc_index_previous_column_resultbody. (exists cfba_gap_previous_column_resultbodybound. cfba_gap_previous_column_resultbodybound + S (cfc_index_previous_column_resultbody) = (k)) -> exists cfc_old_previous_column_resultbody cfc_a_previous_column_resultbody cfc_b_previous_column_resultbody cfc_c_previous_column_resultbody cfc_d_previous_column_resultbody cfc_new_previous_column_resultbody cfc_quotient_previous_column_resultbody. ((exists cfc_state_previous_column_resultbodyprevious. ((exists cfc_left_previous_column_resultbodypreviouscode cfc_right_previous_column_resultbodypreviouscode cfc_matrix_previous_column_resultbodypreviouscode. ((cfc_left_previous_column_resultbodypreviouscode = ((cfc_a_previous_column_resultbody) + (cfc_b_previous_column_resultbody)) * S ((cfc_a_previous_column_resultbody) + (cfc_b_previous_column_resultbody)) + ((cfc_b_previous_column_resultbody) + (cfc_b_previous_column_resultbody))) /\ ((cfc_right_previous_column_resultbodypreviouscode = ((cfc_c_previous_column_resultbody) + (cfc_d_previous_column_resultbody)) * S ((cfc_c_previous_column_resultbody) + (cfc_d_previous_column_resultbody)) + ((cfc_d_previous_column_resultbody) + (cfc_d_previous_column_resultbody))) /\ ((cfc_matrix_previous_column_resultbodypreviouscode = ((cfc_left_previous_column_resultbodypreviouscode) + (cfc_right_previous_column_resultbodypreviouscode)) * S ((cfc_left_previous_column_resultbodypreviouscode) + (cfc_right_previous_column_resultbodypreviouscode)) + ((cfc_right_previous_column_resultbodypreviouscode) + (cfc_right_previous_column_resultbodypreviouscode))) /\ ((cfc_state_previous_column_resultbodyprevious) = ((cfc_old_previous_column_resultbody) + (cfc_matrix_previous_column_resultbodypreviouscode)) * S ((cfc_old_previous_column_resultbody) + (cfc_matrix_previous_column_resultbodypreviouscode)) + ((cfc_matrix_previous_column_resultbodypreviouscode) + (cfc_matrix_previous_column_resultbodypreviouscode))))))) /\ (((exists ff_h_previous_column_resultbodypreviousentry. ff_h_previous_column_resultbodypreviousentry + S (cfc_state_previous_column_resultbodyprevious) = S ((S (cfc_index_previous_column_resultbody)) * cfc_e_previous_column_result)) /\ exists ff_q_previous_column_resultbodypreviousentry. cfc_h_previous_column_result = ff_q_previous_column_resultbodypreviousentry * S ((S (cfc_index_previous_column_resultbody)) * cfc_e_previous_column_result) + (cfc_state_previous_column_resultbodyprevious))))) /\ ((exists cfc_state_previous_column_resultbodyfollowing. ((exists cfc_left_previous_column_resultbodyfollowingcode cfc_right_previous_column_resultbodyfollowingcode cfc_matrix_previous_column_resultbodyfollowingcode. ((cfc_left_previous_column_resultbodyfollowingcode = (((cfc_quotient_previous_column_resultbody * cfc_a_previous_column_resultbody + cfc_c_previous_column_resultbody)) + ((cfc_quotient_previous_column_resultbody * cfc_b_previous_column_resultbody + cfc_d_previous_column_resultbody))) * S (((cfc_quotient_previous_column_resultbody * cfc_a_previous_column_resultbody + cfc_c_previous_column_resultbody)) + ((cfc_quotient_previous_column_resultbody * cfc_b_previous_column_resultbody + cfc_d_previous_column_resultbody))) + (((cfc_quotient_previous_column_resultbody * cfc_b_previous_column_resultbody + cfc_d_previous_column_resultbody)) + ((cfc_quotient_previous_column_resultbody * cfc_b_previous_column_resultbody + cfc_d_previous_column_resultbody)))) /\ ((cfc_right_previous_column_resultbodyfollowingcode = ((cfc_a_previous_column_resultbody) + (cfc_b_previous_column_resultbody)) * S ((cfc_a_previous_column_resultbody) + (cfc_b_previous_column_resultbody)) + ((cfc_b_previous_column_resultbody) + (cfc_b_previous_column_resultbody))) /\ ((cfc_matrix_previous_column_resultbodyfollowingcode = ((cfc_left_previous_column_resultbodyfollowingcode) + (cfc_right_previous_column_resultbodyfollowingcode)) * S ((cfc_left_previous_column_resultbodyfollowingcode) + (cfc_right_previous_column_resultbodyfollowingcode)) + ((cfc_right_previous_column_resultbodyfollowingcode) + (cfc_right_previous_column_resultbodyfollowingcode))) /\ ((cfc_state_previous_column_resultbodyfollowing) = ((cfc_new_previous_column_resultbody) + (cfc_matrix_previous_column_resultbodyfollowingcode)) * S ((cfc_new_previous_column_resultbody) + (cfc_matrix_previous_column_resultbodyfollowingcode)) + ((cfc_matrix_previous_column_resultbodyfollowingcode) + (cfc_matrix_previous_column_resultbodyfollowingcode))))))) /\ (((exists ff_h_previous_column_resultbodyfollowingentry. ff_h_previous_column_resultbodyfollowingentry + S (cfc_state_previous_column_resultbodyfollowing) = S ((S (S cfc_index_previous_column_resultbody)) * cfc_e_previous_column_result)) /\ exists ff_q_previous_column_resultbodyfollowingentry. cfc_h_previous_column_result = ff_q_previous_column_resultbodyfollowingentry * S ((S (S cfc_index_previous_column_resultbody)) * cfc_e_previous_column_result) + (cfc_state_previous_column_resultbodyfollowing))))) /\ (cfc_new_previous_column_resultbody = S ((cfc_quotient_previous_column_resultbody + cfc_old_previous_column_resultbody) * S (cfc_quotient_previous_column_resultbody + cfc_old_previous_column_resultbody) + (cfc_old_previous_column_resultbody + cfc_old_previous_column_resultbody)))))))))

Constructive proof overview

Generated structural guide

The second matrix column is proved to be the actual previous quotient prefix of the same original list, not an arbitrary auxiliary vector chosen to make the determinant or approximation proof work.

The unchanged tactic script uses 6 declared prerequisites and contains 169 exact native proof lines.

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

Proof neighborhood

Direct dependencies

BA0033 cf_convergent_matrix_successor_elimination BA0043 cf_convergent_initial_matrix_exists BA004B cf_convergent_matrix_prefix_functional BA003A cf_convergent_matrix_empty_exists BA0037 cf_convergent_matrix_entry_transport BA003C cf_convergent_matrix_prepend_exists

Direct dependents

BA0050 continued_fraction_adjacent_convergent_determinant

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

169 script commands · 36 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 (6)
cf convergent matrix successor eliminationcf convergent initial matrix existscf convergent matrix prefix functionalcf convergent matrix empty existscf convergent matrix entry transportcf 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 kL1–9

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 s
  3. L3
    intro h
  4. L4
    intro e
  5. L5
    intro u
  6. L6
    intro U
  7. L7
    intro v
  8. L8
    intro V
  9. L9
    intro ht
02Establish hpL10–19

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

  1. L10
    have hp · expand full local formula (707 characters)have hp : ∃ cfc_tail_previous_initial_pred. ∃ cfc_a_previous_initial_pred. ∃ cfc_b_previous_initial_pred. ∃ cfc_c_previous_initial_pred. ∃ cfc_d_previous_initial_pred. ∃ cfc_q_previous_initial_pred. ConvergentMatrixTrace(cfc_tail_previous_initial_pred,h,e,0,cfc_a_previous_initial_pred,cfc_b_previous_initial_pred,cfc_c_previous_initial_pred,cfc_d_previous_initial_pred) ∧ (ListCell(s,cfc_q_previous_initial_pred,cfc_tail_previous_initial_pred) ∧ (u = cfc_q_previous_initial_pred · cfc_a_previous_initial_pred + cfc_c_previous_initial_pred ∧ (U = cfc_q_previous_initial_pred · cfc_b_previous_initial_pred + cfc_d_previous_initial_pred ∧ (v = cfc_a_previous_initial_pred ∧ V = cfc_b_previous_initial_pred))))
    Definitions: ListCellConvergentMatrixTrace
  2. L11
    specialize cf_convergent_matrix_successor_elimination (s)
  3. L12
    specialize cf_convergent_matrix_successor_elimination (h)
  4. L13
    specialize cf_convergent_matrix_successor_elimination (e)
  5. L14
    specialize cf_convergent_matrix_successor_elimination (0)
  6. L15
    specialize cf_convergent_matrix_successor_elimination (u)
  7. L16
    specialize cf_convergent_matrix_successor_elimination (U)
  8. L17
    specialize cf_convergent_matrix_successor_elimination (v)
  9. L18
    specialize cf_convergent_matrix_successor_elimination (V)
  10. L19
    apply cf_convergent_matrix_successor_elimination
03Use earlier factsL20–20

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

  1. L20
    exact ht
04Separate the logical casesL21–30

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

  1. L21
    cases hp
  2. L22
    cases hp_witness
  3. L23
    cases hp_witness_witness
  4. L24
    cases hp_witness_witness_witness
  5. L25
    cases hp_witness_witness_witness_witness
  6. L26
    cases hp_witness_witness_witness_witness_witness
  7. L27
    cases hp_witness_witness_witness_witness_witness_witness
  8. L28
    cases hp_witness_witness_witness_witness_witness_witness_right
  9. L29
    cases hp_witness_witness_witness_witness_witness_witness_right_right
  10. L30
    cases hp_witness_witness_witness_witness_witness_witness_right_right_right
05Separate the logical casesL31–31

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

  1. L31
    cases hp_witness_witness_witness_witness_witness_witness_right_right_right_right
06Establish hmL32–37

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

  1. L32
    have hm : ∃ H. ∃ E. ConvergentMatrixTrace(s,H,E,1,x5,1,1,0)Definitions: ConvergentMatrixTrace
  2. L33
    specialize cf_convergent_initial_matrix_exists (s)
  3. L34
    specialize cf_convergent_initial_matrix_exists (x5)
  4. L35
    specialize cf_convergent_initial_matrix_exists (x)
  5. L36
    apply cf_convergent_initial_matrix_exists
  6. L37
    exact hp_witness_witness_witness_witness_witness_witness_right_left
07Separate the logical casesL38–39

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

  1. L38
    cases hm
  2. L39
    cases hm_witness
08Establish heqL40–49

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

  1. L40
    have heq : ((u = x5) /\ ((U = 1) /\ ((v = 1) /\ (V = 0))))
  2. L41
    specialize cf_convergent_matrix_prefix_functional (1)
  3. L42
    specialize cf_convergent_matrix_prefix_functional (s)
  4. L43
    specialize cf_convergent_matrix_prefix_functional (h)
  5. L44
    specialize cf_convergent_matrix_prefix_functional (e)
  6. L45
    specialize cf_convergent_matrix_prefix_functional (x6)
  7. L46
    specialize cf_convergent_matrix_prefix_functional (x7)
  8. L47
    specialize cf_convergent_matrix_prefix_functional (u)
  9. L48
    specialize cf_convergent_matrix_prefix_functional (U)
  10. L49
    specialize cf_convergent_matrix_prefix_functional (v)
09Use earlier factsL50–57

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

  1. L50
    specialize cf_convergent_matrix_prefix_functional (V)
  2. L51
    specialize cf_convergent_matrix_prefix_functional (x5)
  3. L52
    specialize cf_convergent_matrix_prefix_functional (1)
  4. L53
    specialize cf_convergent_matrix_prefix_functional (1)
  5. L54
    specialize cf_convergent_matrix_prefix_functional (0)
  6. L55
    apply cf_convergent_matrix_prefix_functional
  7. L56
    exact ht
  8. L57
    exact hm_witness_witness
10Separate the logical casesL58–60

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

  1. L58
    cases heq
  2. L59
    cases heq_right
  3. L60
    cases heq_right_right
11Establish hzL61–63

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

  1. L61
    have hz : ∃ H. ∃ E. ConvergentMatrixTrace(s,H,E,0,1,0,0,1)Definitions: ConvergentMatrixTrace
  2. L62
    specialize cf_convergent_matrix_empty_exists (s)
  3. L63
    apply cf_convergent_matrix_empty_exists
12Separate the logical casesL64–65

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

  1. L64
    cases hz
  2. L65
    cases hz_witness
13Construct an explicit witnessL66–69

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

  1. L66
    exists x8
  2. L67
    exists x9
  3. L68
    exists 0
  4. L69
    exists 1
14Use earlier factsL70–79

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

  1. L70
    specialize cf_convergent_matrix_entry_transport (s)
  2. L71
    specialize cf_convergent_matrix_entry_transport (x8)
  3. L72
    specialize cf_convergent_matrix_entry_transport (x9)
  4. L73
    specialize cf_convergent_matrix_entry_transport (0)
  5. L74
    specialize cf_convergent_matrix_entry_transport (U)
  6. L75
    specialize cf_convergent_matrix_entry_transport (0)
  7. L76
    specialize cf_convergent_matrix_entry_transport (V)
  8. L77
    specialize cf_convergent_matrix_entry_transport (1)
  9. L78
    specialize cf_convergent_matrix_entry_transport (1)
  10. L79
    specialize cf_convergent_matrix_entry_transport (0)
15Use earlier factsL80–83

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

  1. L80
    specialize cf_convergent_matrix_entry_transport (0)
  2. L81
    specialize cf_convergent_matrix_entry_transport (1)
  3. L82
    apply cf_convergent_matrix_entry_transport
  4. L83
    exact heq_right_left
16Calculate and transport equalitiesL84–84

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

  1. L84
    refl
17Use earlier factsL85–85

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

  1. L85
    exact heq_right_right_right
18Calculate and transport equalitiesL86–86

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

  1. L86
    refl
19Use earlier factsL87–87

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

  1. L87
    exact hz_witness_witness
20Fix variables and assumptionsL88–95

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

  1. L88
    intro s
  2. L89
    intro h
  3. L90
    intro e
  4. L91
    intro u
  5. L92
    intro U
  6. L93
    intro v
  7. L94
    intro V
  8. L95
    intro ht
21Establish hpL96–105

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

  1. L96
    have hp · expand full local formula (646 characters)have hp : ∃ cfc_tail_previous_step_pred. ∃ cfc_a_previous_step_pred. ∃ cfc_b_previous_step_pred. ∃ cfc_c_previous_step_pred. ∃ cfc_d_previous_step_pred. ∃ cfc_q_previous_step_pred. ConvergentMatrixTrace(cfc_tail_previous_step_pred,h,e,S k,cfc_a_previous_step_pred,cfc_b_previous_step_pred,cfc_c_previous_step_pred,cfc_d_previous_step_pred) ∧ (ListCell(s,cfc_q_previous_step_pred,cfc_tail_previous_step_pred) ∧ (u = cfc_q_previous_step_pred · cfc_a_previous_step_pred + cfc_c_previous_step_pred ∧ (U = cfc_q_previous_step_pred · cfc_b_previous_step_pred + cfc_d_previous_step_pred ∧ (v = cfc_a_previous_step_pred ∧ V = cfc_b_previous_step_pred))))
    Definitions: ListCellConvergentMatrixTrace
  2. L97
    specialize cf_convergent_matrix_successor_elimination (s)
  3. L98
    specialize cf_convergent_matrix_successor_elimination (h)
  4. L99
    specialize cf_convergent_matrix_successor_elimination (e)
  5. L100
    specialize cf_convergent_matrix_successor_elimination (S k)
  6. L101
    specialize cf_convergent_matrix_successor_elimination (u)
  7. L102
    specialize cf_convergent_matrix_successor_elimination (U)
  8. L103
    specialize cf_convergent_matrix_successor_elimination (v)
  9. L104
    specialize cf_convergent_matrix_successor_elimination (V)
  10. L105
    apply cf_convergent_matrix_successor_elimination
22Use earlier factsL106–106

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

  1. L106
    exact ht
23Separate the logical casesL107–116

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

  1. L107
    cases hp
  2. L108
    cases hp_witness
  3. L109
    cases hp_witness_witness
  4. L110
    cases hp_witness_witness_witness
  5. L111
    cases hp_witness_witness_witness_witness
  6. L112
    cases hp_witness_witness_witness_witness_witness
  7. L113
    cases hp_witness_witness_witness_witness_witness_witness
  8. L114
    cases hp_witness_witness_witness_witness_witness_witness_right
  9. L115
    cases hp_witness_witness_witness_witness_witness_witness_right_right
  10. L116
    cases hp_witness_witness_witness_witness_witness_witness_right_right_right
24Separate the logical casesL117–117

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

  1. L117
    cases hp_witness_witness_witness_witness_witness_witness_right_right_right_right
25Establish hiL118–127

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

  1. L118
    have hi : ∃ cfc_h_previous_child. ∃ cfc_e_previous_child. ∃ cfc_p_previous_child. ∃ cfc_q_previous_child. ConvergentMatrixTrace(x,cfc_h_previous_child,cfc_e_previous_child,k,x2,cfc_p_previous_child,x4,cfc_q_previous_child)Definitions: ConvergentMatrixTrace
  2. L119
    specialize IH (x)
  3. L120
    specialize IH (h)
  4. L121
    specialize IH (e)
  5. L122
    specialize IH (x1)
  6. L123
    specialize IH (x2)
  7. L124
    specialize IH (x3)
  8. L125
    specialize IH (x4)
  9. L126
    apply IH
  10. L127
    exact hp_witness_witness_witness_witness_witness_witness_left
26Separate the logical casesL128–131

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

  1. L128
    cases hi
  2. L129
    cases hi_witness
  3. L130
    cases hi_witness_witness
  4. L131
    cases hi_witness_witness_witness
27Establish hextL132–141

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

  1. L132
    have hext : ∃ H. ∃ E. ConvergentMatrixTrace(s,H,E,S k,x5 · x2 + x4,x5 · x8 + x9,x2,x8)Definitions: ConvergentMatrixTrace
  2. L133
    specialize cf_convergent_matrix_prepend_exists (x)
  3. L134
    specialize cf_convergent_matrix_prepend_exists (x6)
  4. L135
    specialize cf_convergent_matrix_prepend_exists (x7)
  5. L136
    specialize cf_convergent_matrix_prepend_exists (k)
  6. L137
    specialize cf_convergent_matrix_prepend_exists (x2)
  7. L138
    specialize cf_convergent_matrix_prepend_exists (x8)
  8. L139
    specialize cf_convergent_matrix_prepend_exists (x4)
  9. L140
    specialize cf_convergent_matrix_prepend_exists (x9)
  10. L141
    specialize cf_convergent_matrix_prepend_exists (x5)
28Use earlier factsL142–145

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

  1. L142
    specialize cf_convergent_matrix_prepend_exists (s)
  2. L143
    apply cf_convergent_matrix_prepend_exists
  3. L144
    exact hi_witness_witness_witness_witness
  4. L145
    exact hp_witness_witness_witness_witness_witness_witness_right_left
29Separate the logical casesL146–147

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

  1. L146
    cases hext
  2. L147
    cases hext_witness
30Construct an explicit witnessL148–151

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

  1. L148
    exists x10
  2. L149
    exists x11
  3. L150
    exists x5 * x8 + x9
  4. L151
    exists x8
31Use earlier factsL152–161

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

  1. L152
    specialize cf_convergent_matrix_entry_transport (s)
  2. L153
    specialize cf_convergent_matrix_entry_transport (x10)
  3. L154
    specialize cf_convergent_matrix_entry_transport (x11)
  4. L155
    specialize cf_convergent_matrix_entry_transport (S k)
  5. L156
    specialize cf_convergent_matrix_entry_transport (U)
  6. L157
    specialize cf_convergent_matrix_entry_transport (x5 * x8 + x9)
  7. L158
    specialize cf_convergent_matrix_entry_transport (V)
  8. L159
    specialize cf_convergent_matrix_entry_transport (x8)
  9. L160
    specialize cf_convergent_matrix_entry_transport ((x5 * x2 + x4))
  10. L161
    specialize cf_convergent_matrix_entry_transport ((x5 * x8 + x9))
32Use earlier factsL162–165

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

  1. L162
    specialize cf_convergent_matrix_entry_transport (x2)
  2. L163
    specialize cf_convergent_matrix_entry_transport (x8)
  3. L164
    apply cf_convergent_matrix_entry_transport
  4. L165
    exact hp_witness_witness_witness_witness_witness_witness_right_right_right_left
33Calculate and transport equalitiesL166–166

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

  1. L166
    refl
34Use earlier factsL167–167

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

  1. L167
    exact hp_witness_witness_witness_witness_witness_witness_right_right_right_right_right
35Calculate and transport equalitiesL168–168

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

  1. L168
    refl
36Use earlier factsL169–169

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

  1. L169
    exact hext_witness_witness

Library-wide reading audit

Original exact command ledger · 169 lines
  1. 0001induction k
  2. 0002intro s
  3. 0003intro h
  4. 0004intro e
  5. 0005intro u
  6. 0006intro U
  7. 0007intro v
  8. 0008intro V
  9. 0009intro ht
  10. 0010have hp : exists cfc_tail_previous_initial_pred cfc_a_previous_initial_pred cfc_b_previous_initial_pred cfc_c_previous_initial_pred cfc_d_previous_initial_pred cfc_q_previous_initial_pred. ((exists cfc_tail_previous_initial_predprefix. ((exists cfc_state_previous_initial_predprefixinitial. ((exists cfc_left_previous_initial_predprefixinitialcode cfc_right_previous_initial_predprefixinitialcode cfc_matrix_previous_initial_predprefixinitialcode. ((cfc_left_previous_initial_predprefixinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_previous_initial_predprefixinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_previous_initial_predprefixinitialcode = ((cfc_left_previous_initial_predprefixinitialcode) + (cfc_right_previous_initial_predprefixinitialcode)) * S ((cfc_left_previous_initial_predprefixinitialcode) + (cfc_right_previous_initial_predprefixinitialcode)) + ((cfc_right_previous_initial_predprefixinitialcode) + (cfc_right_previous_initial_predprefixinitialcode))) /\ ((cfc_state_previous_initial_predprefixinitial) = ((cfc_tail_previous_initial_predprefix) + (cfc_matrix_previous_initial_predprefixinitialcode)) * S ((cfc_tail_previous_initial_predprefix) + (cfc_matrix_previous_initial_predprefixinitialcode)) + ((cfc_matrix_previous_initial_predprefixinitialcode) + (cfc_matrix_previous_initial_predprefixinitialcode))))))) /\ (((exists ff_h_previous_initial_predprefixinitialentry. ff_h_previous_initial_predprefixinitialentry + S (cfc_state_previous_initial_predprefixinitial) = S ((S (0)) * e)) /\ exists ff_q_previous_initial_predprefixinitialentry. h = ff_q_previous_initial_predprefixinitialentry * S ((S (0)) * e) + (cfc_state_previous_initial_predprefixinitial))))) /\ ((exists cfc_state_previous_initial_predprefixterminal. ((exists cfc_left_previous_initial_predprefixterminalcode cfc_right_previous_initial_predprefixterminalcode cfc_matrix_previous_initial_predprefixterminalcode. ((cfc_left_previous_initial_predprefixterminalcode = ((cfc_a_previous_initial_pred) + (cfc_b_previous_initial_pred)) * S ((cfc_a_previous_initial_pred) + (cfc_b_previous_initial_pred)) + ((cfc_b_previous_initial_pred) + (cfc_b_previous_initial_pred))) /\ ((cfc_right_previous_initial_predprefixterminalcode = ((cfc_c_previous_initial_pred) + (cfc_d_previous_initial_pred)) * S ((cfc_c_previous_initial_pred) + (cfc_d_previous_initial_pred)) + ((cfc_d_previous_initial_pred) + (cfc_d_previous_initial_pred))) /\ ((cfc_matrix_previous_initial_predprefixterminalcode = ((cfc_left_previous_initial_predprefixterminalcode) + (cfc_right_previous_initial_predprefixterminalcode)) * S ((cfc_left_previous_initial_predprefixterminalcode) + (cfc_right_previous_initial_predprefixterminalcode)) + ((cfc_right_previous_initial_predprefixterminalcode) + (cfc_right_previous_initial_predprefixterminalcode))) /\ ((cfc_state_previous_initial_predprefixterminal) = ((cfc_tail_previous_initial_pred) + (cfc_matrix_previous_initial_predprefixterminalcode)) * S ((cfc_tail_previous_initial_pred) + (cfc_matrix_previous_initial_predprefixterminalcode)) + ((cfc_matrix_previous_initial_predprefixterminalcode) + (cfc_matrix_previous_initial_predprefixterminalcode))))))) /\ (((exists ff_h_previous_initial_predprefixterminalentry. ff_h_previous_initial_predprefixterminalentry + S (cfc_state_previous_initial_predprefixterminal) = S ((S (0)) * e)) /\ exists ff_q_previous_initial_predprefixterminalentry. h = ff_q_previous_initial_predprefixterminalentry * S ((S (0)) * e) + (cfc_state_previous_initial_predprefixterminal))))) /\ (forall cfc_index_previous_initial_predprefix. (exists cfba_gap_previous_initial_predprefixbound. cfba_gap_previous_initial_predprefixbound + S (cfc_index_previous_initial_predprefix) = (0)) -> exists cfc_old_previous_initial_predprefix cfc_a_previous_initial_predprefix cfc_b_previous_initial_predprefix cfc_c_previous_initial_predprefix cfc_d_previous_initial_predprefix cfc_new_previous_initial_predprefix cfc_quotient_previous_initial_predprefix. ((exists cfc_state_previous_initial_predprefixprevious. ((exists cfc_left_previous_initial_predprefixpreviouscode cfc_right_previous_initial_predprefixpreviouscode cfc_matrix_previous_initial_predprefixpreviouscode. ((cfc_left_previous_initial_predprefixpreviouscode = ((cfc_a_previous_initial_predprefix) + (cfc_b_previous_initial_predprefix)) * S ((cfc_a_previous_initial_predprefix) + (cfc_b_previous_initial_predprefix)) + ((cfc_b_previous_initial_predprefix) + (cfc_b_previous_initial_predprefix))) /\ ((cfc_right_previous_initial_predprefixpreviouscode = ((cfc_c_previous_initial_predprefix) + (cfc_d_previous_initial_predprefix)) * S ((cfc_c_previous_initial_predprefix) + (cfc_d_previous_initial_predprefix)) + ((cfc_d_previous_initial_predprefix) + (cfc_d_previous_initial_predprefix))) /\ ((cfc_matrix_previous_initial_predprefixpreviouscode = ((cfc_left_previous_initial_predprefixpreviouscode) + (cfc_right_previous_initial_predprefixpreviouscode)) * S ((cfc_left_previous_initial_predprefixpreviouscode) + (cfc_right_previous_initial_predprefixpreviouscode)) + ((cfc_right_previous_initial_predprefixpreviouscode) + (cfc_right_previous_initial_predprefixpreviouscode))) /\ ((cfc_state_previous_initial_predprefixprevious) = ((cfc_old_previous_initial_predprefix) + (cfc_matrix_previous_initial_predprefixpreviouscode)) * S ((cfc_old_previous_initial_predprefix) + (cfc_matrix_previous_initial_predprefixpreviouscode)) + ((cfc_matrix_previous_initial_predprefixpreviouscode) + (cfc_matrix_previous_initial_predprefixpreviouscode))))))) /\ (((exists ff_h_previous_initial_predprefixpreviousentry. ff_h_previous_initial_predprefixpreviousentry + S (cfc_state_previous_initial_predprefixprevious) = S ((S (cfc_index_previous_initial_predprefix)) * e)) /\ exists ff_q_previous_initial_predprefixpreviousentry. h = ff_q_previous_initial_predprefixpreviousentry * S ((S (cfc_index_previous_initial_predprefix)) * e) + (cfc_state_previous_initial_predprefixprevious))))) /\ ((exists cfc_state_previous_initial_predprefixfollowing. ((exists cfc_left_previous_initial_predprefixfollowingcode cfc_right_previous_initial_predprefixfollowingcode cfc_matrix_previous_initial_predprefixfollowingcode. ((cfc_left_previous_initial_predprefixfollowingcode = (((cfc_quotient_previous_initial_predprefix * cfc_a_previous_initial_predprefix + cfc_c_previous_initial_predprefix)) + ((cfc_quotient_previous_initial_predprefix * cfc_b_previous_initial_predprefix + cfc_d_previous_initial_predprefix))) * S (((cfc_quotient_previous_initial_predprefix * cfc_a_previous_initial_predprefix + cfc_c_previous_initial_predprefix)) + ((cfc_quotient_previous_initial_predprefix * cfc_b_previous_initial_predprefix + cfc_d_previous_initial_predprefix))) + (((cfc_quotient_previous_initial_predprefix * cfc_b_previous_initial_predprefix + cfc_d_previous_initial_predprefix)) + ((cfc_quotient_previous_initial_predprefix * cfc_b_previous_initial_predprefix + cfc_d_previous_initial_predprefix)))) /\ ((cfc_right_previous_initial_predprefixfollowingcode = ((cfc_a_previous_initial_predprefix) + (cfc_b_previous_initial_predprefix)) * S ((cfc_a_previous_initial_predprefix) + (cfc_b_previous_initial_predprefix)) + ((cfc_b_previous_initial_predprefix) + (cfc_b_previous_initial_predprefix))) /\ ((cfc_matrix_previous_initial_predprefixfollowingcode = ((cfc_left_previous_initial_predprefixfollowingcode) + (cfc_right_previous_initial_predprefixfollowingcode)) * S ((cfc_left_previous_initial_predprefixfollowingcode) + (cfc_right_previous_initial_predprefixfollowingcode)) + ((cfc_right_previous_initial_predprefixfollowingcode) + (cfc_right_previous_initial_predprefixfollowingcode))) /\ ((cfc_state_previous_initial_predprefixfollowing) = ((cfc_new_previous_initial_predprefix) + (cfc_matrix_previous_initial_predprefixfollowingcode)) * S ((cfc_new_previous_initial_predprefix) + (cfc_matrix_previous_initial_predprefixfollowingcode)) + ((cfc_matrix_previous_initial_predprefixfollowingcode) + (cfc_matrix_previous_initial_predprefixfollowingcode))))))) /\ (((exists ff_h_previous_initial_predprefixfollowingentry. ff_h_previous_initial_predprefixfollowingentry + S (cfc_state_previous_initial_predprefixfollowing) = S ((S (S cfc_index_previous_initial_predprefix)) * e)) /\ exists ff_q_previous_initial_predprefixfollowingentry. h = ff_q_previous_initial_predprefixfollowingentry * S ((S (S cfc_index_previous_initial_predprefix)) * e) + (cfc_state_previous_initial_predprefixfollowing))))) /\ (cfc_new_previous_initial_predprefix = S ((cfc_quotient_previous_initial_predprefix + cfc_old_previous_initial_predprefix) * S (cfc_quotient_previous_initial_predprefix + cfc_old_previous_initial_predprefix) + (cfc_old_previous_initial_predprefix + cfc_old_previous_initial_predprefix))))))))) /\ ((s = S ((cfc_q_previous_initial_pred + cfc_tail_previous_initial_pred) * S (cfc_q_previous_initial_pred + cfc_tail_previous_initial_pred) + (cfc_tail_previous_initial_pred + cfc_tail_previous_initial_pred))) /\ (((u) = cfc_q_previous_initial_pred * cfc_a_previous_initial_pred + cfc_c_previous_initial_pred) /\ (((U) = cfc_q_previous_initial_pred * cfc_b_previous_initial_pred + cfc_d_previous_initial_pred) /\ (((v) = cfc_a_previous_initial_pred) /\ ((V) = cfc_b_previous_initial_pred))))))
  11. 0011specialize cf_convergent_matrix_successor_elimination (s)
  12. 0012specialize cf_convergent_matrix_successor_elimination (h)
  13. 0013specialize cf_convergent_matrix_successor_elimination (e)
  14. 0014specialize cf_convergent_matrix_successor_elimination (0)
  15. 0015specialize cf_convergent_matrix_successor_elimination (u)
  16. 0016specialize cf_convergent_matrix_successor_elimination (U)
  17. 0017specialize cf_convergent_matrix_successor_elimination (v)
  18. 0018specialize cf_convergent_matrix_successor_elimination (V)
  19. 0019apply cf_convergent_matrix_successor_elimination
  20. 0020exact ht
  21. 0021cases hp
  22. 0022cases hp_witness
  23. 0023cases hp_witness_witness
  24. 0024cases hp_witness_witness_witness
  25. 0025cases hp_witness_witness_witness_witness
  26. 0026cases hp_witness_witness_witness_witness_witness
  27. 0027cases hp_witness_witness_witness_witness_witness_witness
  28. 0028cases hp_witness_witness_witness_witness_witness_witness_right
  29. 0029cases hp_witness_witness_witness_witness_witness_witness_right_right
  30. 0030cases hp_witness_witness_witness_witness_witness_witness_right_right_right
  31. 0031cases hp_witness_witness_witness_witness_witness_witness_right_right_right_right
  32. 0032have hm : exists H E. exists cfc_tail_previous_initial_matrix. ((exists cfc_state_previous_initial_matrixinitial. ((exists cfc_left_previous_initial_matrixinitialcode cfc_right_previous_initial_matrixinitialcode cfc_matrix_previous_initial_matrixinitialcode. ((cfc_left_previous_initial_matrixinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_previous_initial_matrixinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_previous_initial_matrixinitialcode = ((cfc_left_previous_initial_matrixinitialcode) + (cfc_right_previous_initial_matrixinitialcode)) * S ((cfc_left_previous_initial_matrixinitialcode) + (cfc_right_previous_initial_matrixinitialcode)) + ((cfc_right_previous_initial_matrixinitialcode) + (cfc_right_previous_initial_matrixinitialcode))) /\ ((cfc_state_previous_initial_matrixinitial) = ((cfc_tail_previous_initial_matrix) + (cfc_matrix_previous_initial_matrixinitialcode)) * S ((cfc_tail_previous_initial_matrix) + (cfc_matrix_previous_initial_matrixinitialcode)) + ((cfc_matrix_previous_initial_matrixinitialcode) + (cfc_matrix_previous_initial_matrixinitialcode))))))) /\ (((exists ff_h_previous_initial_matrixinitialentry. ff_h_previous_initial_matrixinitialentry + S (cfc_state_previous_initial_matrixinitial) = S ((S (0)) * E)) /\ exists ff_q_previous_initial_matrixinitialentry. H = ff_q_previous_initial_matrixinitialentry * S ((S (0)) * E) + (cfc_state_previous_initial_matrixinitial))))) /\ ((exists cfc_state_previous_initial_matrixterminal. ((exists cfc_left_previous_initial_matrixterminalcode cfc_right_previous_initial_matrixterminalcode cfc_matrix_previous_initial_matrixterminalcode. ((cfc_left_previous_initial_matrixterminalcode = ((x5) + (1)) * S ((x5) + (1)) + ((1) + (1))) /\ ((cfc_right_previous_initial_matrixterminalcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_matrix_previous_initial_matrixterminalcode = ((cfc_left_previous_initial_matrixterminalcode) + (cfc_right_previous_initial_matrixterminalcode)) * S ((cfc_left_previous_initial_matrixterminalcode) + (cfc_right_previous_initial_matrixterminalcode)) + ((cfc_right_previous_initial_matrixterminalcode) + (cfc_right_previous_initial_matrixterminalcode))) /\ ((cfc_state_previous_initial_matrixterminal) = ((s) + (cfc_matrix_previous_initial_matrixterminalcode)) * S ((s) + (cfc_matrix_previous_initial_matrixterminalcode)) + ((cfc_matrix_previous_initial_matrixterminalcode) + (cfc_matrix_previous_initial_matrixterminalcode))))))) /\ (((exists ff_h_previous_initial_matrixterminalentry. ff_h_previous_initial_matrixterminalentry + S (cfc_state_previous_initial_matrixterminal) = S ((S (1)) * E)) /\ exists ff_q_previous_initial_matrixterminalentry. H = ff_q_previous_initial_matrixterminalentry * S ((S (1)) * E) + (cfc_state_previous_initial_matrixterminal))))) /\ (forall cfc_index_previous_initial_matrix. (exists cfba_gap_previous_initial_matrixbound. cfba_gap_previous_initial_matrixbound + S (cfc_index_previous_initial_matrix) = (1)) -> exists cfc_old_previous_initial_matrix cfc_a_previous_initial_matrix cfc_b_previous_initial_matrix cfc_c_previous_initial_matrix cfc_d_previous_initial_matrix cfc_new_previous_initial_matrix cfc_quotient_previous_initial_matrix. ((exists cfc_state_previous_initial_matrixprevious. ((exists cfc_left_previous_initial_matrixpreviouscode cfc_right_previous_initial_matrixpreviouscode cfc_matrix_previous_initial_matrixpreviouscode. ((cfc_left_previous_initial_matrixpreviouscode = ((cfc_a_previous_initial_matrix) + (cfc_b_previous_initial_matrix)) * S ((cfc_a_previous_initial_matrix) + (cfc_b_previous_initial_matrix)) + ((cfc_b_previous_initial_matrix) + (cfc_b_previous_initial_matrix))) /\ ((cfc_right_previous_initial_matrixpreviouscode = ((cfc_c_previous_initial_matrix) + (cfc_d_previous_initial_matrix)) * S ((cfc_c_previous_initial_matrix) + (cfc_d_previous_initial_matrix)) + ((cfc_d_previous_initial_matrix) + (cfc_d_previous_initial_matrix))) /\ ((cfc_matrix_previous_initial_matrixpreviouscode = ((cfc_left_previous_initial_matrixpreviouscode) + (cfc_right_previous_initial_matrixpreviouscode)) * S ((cfc_left_previous_initial_matrixpreviouscode) + (cfc_right_previous_initial_matrixpreviouscode)) + ((cfc_right_previous_initial_matrixpreviouscode) + (cfc_right_previous_initial_matrixpreviouscode))) /\ ((cfc_state_previous_initial_matrixprevious) = ((cfc_old_previous_initial_matrix) + (cfc_matrix_previous_initial_matrixpreviouscode)) * S ((cfc_old_previous_initial_matrix) + (cfc_matrix_previous_initial_matrixpreviouscode)) + ((cfc_matrix_previous_initial_matrixpreviouscode) + (cfc_matrix_previous_initial_matrixpreviouscode))))))) /\ (((exists ff_h_previous_initial_matrixpreviousentry. ff_h_previous_initial_matrixpreviousentry + S (cfc_state_previous_initial_matrixprevious) = S ((S (cfc_index_previous_initial_matrix)) * E)) /\ exists ff_q_previous_initial_matrixpreviousentry. H = ff_q_previous_initial_matrixpreviousentry * S ((S (cfc_index_previous_initial_matrix)) * E) + (cfc_state_previous_initial_matrixprevious))))) /\ ((exists cfc_state_previous_initial_matrixfollowing. ((exists cfc_left_previous_initial_matrixfollowingcode cfc_right_previous_initial_matrixfollowingcode cfc_matrix_previous_initial_matrixfollowingcode. ((cfc_left_previous_initial_matrixfollowingcode = (((cfc_quotient_previous_initial_matrix * cfc_a_previous_initial_matrix + cfc_c_previous_initial_matrix)) + ((cfc_quotient_previous_initial_matrix * cfc_b_previous_initial_matrix + cfc_d_previous_initial_matrix))) * S (((cfc_quotient_previous_initial_matrix * cfc_a_previous_initial_matrix + cfc_c_previous_initial_matrix)) + ((cfc_quotient_previous_initial_matrix * cfc_b_previous_initial_matrix + cfc_d_previous_initial_matrix))) + (((cfc_quotient_previous_initial_matrix * cfc_b_previous_initial_matrix + cfc_d_previous_initial_matrix)) + ((cfc_quotient_previous_initial_matrix * cfc_b_previous_initial_matrix + cfc_d_previous_initial_matrix)))) /\ ((cfc_right_previous_initial_matrixfollowingcode = ((cfc_a_previous_initial_matrix) + (cfc_b_previous_initial_matrix)) * S ((cfc_a_previous_initial_matrix) + (cfc_b_previous_initial_matrix)) + ((cfc_b_previous_initial_matrix) + (cfc_b_previous_initial_matrix))) /\ ((cfc_matrix_previous_initial_matrixfollowingcode = ((cfc_left_previous_initial_matrixfollowingcode) + (cfc_right_previous_initial_matrixfollowingcode)) * S ((cfc_left_previous_initial_matrixfollowingcode) + (cfc_right_previous_initial_matrixfollowingcode)) + ((cfc_right_previous_initial_matrixfollowingcode) + (cfc_right_previous_initial_matrixfollowingcode))) /\ ((cfc_state_previous_initial_matrixfollowing) = ((cfc_new_previous_initial_matrix) + (cfc_matrix_previous_initial_matrixfollowingcode)) * S ((cfc_new_previous_initial_matrix) + (cfc_matrix_previous_initial_matrixfollowingcode)) + ((cfc_matrix_previous_initial_matrixfollowingcode) + (cfc_matrix_previous_initial_matrixfollowingcode))))))) /\ (((exists ff_h_previous_initial_matrixfollowingentry. ff_h_previous_initial_matrixfollowingentry + S (cfc_state_previous_initial_matrixfollowing) = S ((S (S cfc_index_previous_initial_matrix)) * E)) /\ exists ff_q_previous_initial_matrixfollowingentry. H = ff_q_previous_initial_matrixfollowingentry * S ((S (S cfc_index_previous_initial_matrix)) * E) + (cfc_state_previous_initial_matrixfollowing))))) /\ (cfc_new_previous_initial_matrix = S ((cfc_quotient_previous_initial_matrix + cfc_old_previous_initial_matrix) * S (cfc_quotient_previous_initial_matrix + cfc_old_previous_initial_matrix) + (cfc_old_previous_initial_matrix + cfc_old_previous_initial_matrix))))))))
  33. 0033specialize cf_convergent_initial_matrix_exists (s)
  34. 0034specialize cf_convergent_initial_matrix_exists (x5)
  35. 0035specialize cf_convergent_initial_matrix_exists (x)
  36. 0036apply cf_convergent_initial_matrix_exists
  37. 0037exact hp_witness_witness_witness_witness_witness_witness_right_left
  38. 0038cases hm
  39. 0039cases hm_witness
  40. 0040have heq : ((u = x5) /\ ((U = 1) /\ ((v = 1) /\ (V = 0))))
  41. 0041specialize cf_convergent_matrix_prefix_functional (1)
  42. 0042specialize cf_convergent_matrix_prefix_functional (s)
  43. 0043specialize cf_convergent_matrix_prefix_functional (h)
  44. 0044specialize cf_convergent_matrix_prefix_functional (e)
  45. 0045specialize cf_convergent_matrix_prefix_functional (x6)
  46. 0046specialize cf_convergent_matrix_prefix_functional (x7)
  47. 0047specialize cf_convergent_matrix_prefix_functional (u)
  48. 0048specialize cf_convergent_matrix_prefix_functional (U)
  49. 0049specialize cf_convergent_matrix_prefix_functional (v)
  50. 0050specialize cf_convergent_matrix_prefix_functional (V)
  51. 0051specialize cf_convergent_matrix_prefix_functional (x5)
  52. 0052specialize cf_convergent_matrix_prefix_functional (1)
  53. 0053specialize cf_convergent_matrix_prefix_functional (1)
  54. 0054specialize cf_convergent_matrix_prefix_functional (0)
  55. 0055apply cf_convergent_matrix_prefix_functional
  56. 0056exact ht
  57. 0057exact hm_witness_witness
  58. 0058cases heq
  59. 0059cases heq_right
  60. 0060cases heq_right_right
  61. 0061have hz : exists H E. exists cfc_tail_previous_empty. ((exists cfc_state_previous_emptyinitial. ((exists cfc_left_previous_emptyinitialcode cfc_right_previous_emptyinitialcode cfc_matrix_previous_emptyinitialcode. ((cfc_left_previous_emptyinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_previous_emptyinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_previous_emptyinitialcode = ((cfc_left_previous_emptyinitialcode) + (cfc_right_previous_emptyinitialcode)) * S ((cfc_left_previous_emptyinitialcode) + (cfc_right_previous_emptyinitialcode)) + ((cfc_right_previous_emptyinitialcode) + (cfc_right_previous_emptyinitialcode))) /\ ((cfc_state_previous_emptyinitial) = ((cfc_tail_previous_empty) + (cfc_matrix_previous_emptyinitialcode)) * S ((cfc_tail_previous_empty) + (cfc_matrix_previous_emptyinitialcode)) + ((cfc_matrix_previous_emptyinitialcode) + (cfc_matrix_previous_emptyinitialcode))))))) /\ (((exists ff_h_previous_emptyinitialentry. ff_h_previous_emptyinitialentry + S (cfc_state_previous_emptyinitial) = S ((S (0)) * E)) /\ exists ff_q_previous_emptyinitialentry. H = ff_q_previous_emptyinitialentry * S ((S (0)) * E) + (cfc_state_previous_emptyinitial))))) /\ ((exists cfc_state_previous_emptyterminal. ((exists cfc_left_previous_emptyterminalcode cfc_right_previous_emptyterminalcode cfc_matrix_previous_emptyterminalcode. ((cfc_left_previous_emptyterminalcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_previous_emptyterminalcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_previous_emptyterminalcode = ((cfc_left_previous_emptyterminalcode) + (cfc_right_previous_emptyterminalcode)) * S ((cfc_left_previous_emptyterminalcode) + (cfc_right_previous_emptyterminalcode)) + ((cfc_right_previous_emptyterminalcode) + (cfc_right_previous_emptyterminalcode))) /\ ((cfc_state_previous_emptyterminal) = ((s) + (cfc_matrix_previous_emptyterminalcode)) * S ((s) + (cfc_matrix_previous_emptyterminalcode)) + ((cfc_matrix_previous_emptyterminalcode) + (cfc_matrix_previous_emptyterminalcode))))))) /\ (((exists ff_h_previous_emptyterminalentry. ff_h_previous_emptyterminalentry + S (cfc_state_previous_emptyterminal) = S ((S (0)) * E)) /\ exists ff_q_previous_emptyterminalentry. H = ff_q_previous_emptyterminalentry * S ((S (0)) * E) + (cfc_state_previous_emptyterminal))))) /\ (forall cfc_index_previous_empty. (exists cfba_gap_previous_emptybound. cfba_gap_previous_emptybound + S (cfc_index_previous_empty) = (0)) -> exists cfc_old_previous_empty cfc_a_previous_empty cfc_b_previous_empty cfc_c_previous_empty cfc_d_previous_empty cfc_new_previous_empty cfc_quotient_previous_empty. ((exists cfc_state_previous_emptyprevious. ((exists cfc_left_previous_emptypreviouscode cfc_right_previous_emptypreviouscode cfc_matrix_previous_emptypreviouscode. ((cfc_left_previous_emptypreviouscode = ((cfc_a_previous_empty) + (cfc_b_previous_empty)) * S ((cfc_a_previous_empty) + (cfc_b_previous_empty)) + ((cfc_b_previous_empty) + (cfc_b_previous_empty))) /\ ((cfc_right_previous_emptypreviouscode = ((cfc_c_previous_empty) + (cfc_d_previous_empty)) * S ((cfc_c_previous_empty) + (cfc_d_previous_empty)) + ((cfc_d_previous_empty) + (cfc_d_previous_empty))) /\ ((cfc_matrix_previous_emptypreviouscode = ((cfc_left_previous_emptypreviouscode) + (cfc_right_previous_emptypreviouscode)) * S ((cfc_left_previous_emptypreviouscode) + (cfc_right_previous_emptypreviouscode)) + ((cfc_right_previous_emptypreviouscode) + (cfc_right_previous_emptypreviouscode))) /\ ((cfc_state_previous_emptyprevious) = ((cfc_old_previous_empty) + (cfc_matrix_previous_emptypreviouscode)) * S ((cfc_old_previous_empty) + (cfc_matrix_previous_emptypreviouscode)) + ((cfc_matrix_previous_emptypreviouscode) + (cfc_matrix_previous_emptypreviouscode))))))) /\ (((exists ff_h_previous_emptypreviousentry. ff_h_previous_emptypreviousentry + S (cfc_state_previous_emptyprevious) = S ((S (cfc_index_previous_empty)) * E)) /\ exists ff_q_previous_emptypreviousentry. H = ff_q_previous_emptypreviousentry * S ((S (cfc_index_previous_empty)) * E) + (cfc_state_previous_emptyprevious))))) /\ ((exists cfc_state_previous_emptyfollowing. ((exists cfc_left_previous_emptyfollowingcode cfc_right_previous_emptyfollowingcode cfc_matrix_previous_emptyfollowingcode. ((cfc_left_previous_emptyfollowingcode = (((cfc_quotient_previous_empty * cfc_a_previous_empty + cfc_c_previous_empty)) + ((cfc_quotient_previous_empty * cfc_b_previous_empty + cfc_d_previous_empty))) * S (((cfc_quotient_previous_empty * cfc_a_previous_empty + cfc_c_previous_empty)) + ((cfc_quotient_previous_empty * cfc_b_previous_empty + cfc_d_previous_empty))) + (((cfc_quotient_previous_empty * cfc_b_previous_empty + cfc_d_previous_empty)) + ((cfc_quotient_previous_empty * cfc_b_previous_empty + cfc_d_previous_empty)))) /\ ((cfc_right_previous_emptyfollowingcode = ((cfc_a_previous_empty) + (cfc_b_previous_empty)) * S ((cfc_a_previous_empty) + (cfc_b_previous_empty)) + ((cfc_b_previous_empty) + (cfc_b_previous_empty))) /\ ((cfc_matrix_previous_emptyfollowingcode = ((cfc_left_previous_emptyfollowingcode) + (cfc_right_previous_emptyfollowingcode)) * S ((cfc_left_previous_emptyfollowingcode) + (cfc_right_previous_emptyfollowingcode)) + ((cfc_right_previous_emptyfollowingcode) + (cfc_right_previous_emptyfollowingcode))) /\ ((cfc_state_previous_emptyfollowing) = ((cfc_new_previous_empty) + (cfc_matrix_previous_emptyfollowingcode)) * S ((cfc_new_previous_empty) + (cfc_matrix_previous_emptyfollowingcode)) + ((cfc_matrix_previous_emptyfollowingcode) + (cfc_matrix_previous_emptyfollowingcode))))))) /\ (((exists ff_h_previous_emptyfollowingentry. ff_h_previous_emptyfollowingentry + S (cfc_state_previous_emptyfollowing) = S ((S (S cfc_index_previous_empty)) * E)) /\ exists ff_q_previous_emptyfollowingentry. H = ff_q_previous_emptyfollowingentry * S ((S (S cfc_index_previous_empty)) * E) + (cfc_state_previous_emptyfollowing))))) /\ (cfc_new_previous_empty = S ((cfc_quotient_previous_empty + cfc_old_previous_empty) * S (cfc_quotient_previous_empty + cfc_old_previous_empty) + (cfc_old_previous_empty + cfc_old_previous_empty))))))))
  62. 0062specialize cf_convergent_matrix_empty_exists (s)
  63. 0063apply cf_convergent_matrix_empty_exists
  64. 0064cases hz
  65. 0065cases hz_witness
  66. 0066exists x8
  67. 0067exists x9
  68. 0068exists 0
  69. 0069exists 1
  70. 0070specialize cf_convergent_matrix_entry_transport (s)
  71. 0071specialize cf_convergent_matrix_entry_transport (x8)
  72. 0072specialize cf_convergent_matrix_entry_transport (x9)
  73. 0073specialize cf_convergent_matrix_entry_transport (0)
  74. 0074specialize cf_convergent_matrix_entry_transport (U)
  75. 0075specialize cf_convergent_matrix_entry_transport (0)
  76. 0076specialize cf_convergent_matrix_entry_transport (V)
  77. 0077specialize cf_convergent_matrix_entry_transport (1)
  78. 0078specialize cf_convergent_matrix_entry_transport (1)
  79. 0079specialize cf_convergent_matrix_entry_transport (0)
  80. 0080specialize cf_convergent_matrix_entry_transport (0)
  81. 0081specialize cf_convergent_matrix_entry_transport (1)
  82. 0082apply cf_convergent_matrix_entry_transport
  83. 0083exact heq_right_left
  84. 0084refl
  85. 0085exact heq_right_right_right
  86. 0086refl
  87. 0087exact hz_witness_witness
  88. 0088intro s
  89. 0089intro h
  90. 0090intro e
  91. 0091intro u
  92. 0092intro U
  93. 0093intro v
  94. 0094intro V
  95. 0095intro ht
  96. 0096have hp : exists cfc_tail_previous_step_pred cfc_a_previous_step_pred cfc_b_previous_step_pred cfc_c_previous_step_pred cfc_d_previous_step_pred cfc_q_previous_step_pred. ((exists cfc_tail_previous_step_predprefix. ((exists cfc_state_previous_step_predprefixinitial. ((exists cfc_left_previous_step_predprefixinitialcode cfc_right_previous_step_predprefixinitialcode cfc_matrix_previous_step_predprefixinitialcode. ((cfc_left_previous_step_predprefixinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_previous_step_predprefixinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_previous_step_predprefixinitialcode = ((cfc_left_previous_step_predprefixinitialcode) + (cfc_right_previous_step_predprefixinitialcode)) * S ((cfc_left_previous_step_predprefixinitialcode) + (cfc_right_previous_step_predprefixinitialcode)) + ((cfc_right_previous_step_predprefixinitialcode) + (cfc_right_previous_step_predprefixinitialcode))) /\ ((cfc_state_previous_step_predprefixinitial) = ((cfc_tail_previous_step_predprefix) + (cfc_matrix_previous_step_predprefixinitialcode)) * S ((cfc_tail_previous_step_predprefix) + (cfc_matrix_previous_step_predprefixinitialcode)) + ((cfc_matrix_previous_step_predprefixinitialcode) + (cfc_matrix_previous_step_predprefixinitialcode))))))) /\ (((exists ff_h_previous_step_predprefixinitialentry. ff_h_previous_step_predprefixinitialentry + S (cfc_state_previous_step_predprefixinitial) = S ((S (0)) * e)) /\ exists ff_q_previous_step_predprefixinitialentry. h = ff_q_previous_step_predprefixinitialentry * S ((S (0)) * e) + (cfc_state_previous_step_predprefixinitial))))) /\ ((exists cfc_state_previous_step_predprefixterminal. ((exists cfc_left_previous_step_predprefixterminalcode cfc_right_previous_step_predprefixterminalcode cfc_matrix_previous_step_predprefixterminalcode. ((cfc_left_previous_step_predprefixterminalcode = ((cfc_a_previous_step_pred) + (cfc_b_previous_step_pred)) * S ((cfc_a_previous_step_pred) + (cfc_b_previous_step_pred)) + ((cfc_b_previous_step_pred) + (cfc_b_previous_step_pred))) /\ ((cfc_right_previous_step_predprefixterminalcode = ((cfc_c_previous_step_pred) + (cfc_d_previous_step_pred)) * S ((cfc_c_previous_step_pred) + (cfc_d_previous_step_pred)) + ((cfc_d_previous_step_pred) + (cfc_d_previous_step_pred))) /\ ((cfc_matrix_previous_step_predprefixterminalcode = ((cfc_left_previous_step_predprefixterminalcode) + (cfc_right_previous_step_predprefixterminalcode)) * S ((cfc_left_previous_step_predprefixterminalcode) + (cfc_right_previous_step_predprefixterminalcode)) + ((cfc_right_previous_step_predprefixterminalcode) + (cfc_right_previous_step_predprefixterminalcode))) /\ ((cfc_state_previous_step_predprefixterminal) = ((cfc_tail_previous_step_pred) + (cfc_matrix_previous_step_predprefixterminalcode)) * S ((cfc_tail_previous_step_pred) + (cfc_matrix_previous_step_predprefixterminalcode)) + ((cfc_matrix_previous_step_predprefixterminalcode) + (cfc_matrix_previous_step_predprefixterminalcode))))))) /\ (((exists ff_h_previous_step_predprefixterminalentry. ff_h_previous_step_predprefixterminalentry + S (cfc_state_previous_step_predprefixterminal) = S ((S (S k)) * e)) /\ exists ff_q_previous_step_predprefixterminalentry. h = ff_q_previous_step_predprefixterminalentry * S ((S (S k)) * e) + (cfc_state_previous_step_predprefixterminal))))) /\ (forall cfc_index_previous_step_predprefix. (exists cfba_gap_previous_step_predprefixbound. cfba_gap_previous_step_predprefixbound + S (cfc_index_previous_step_predprefix) = (S k)) -> exists cfc_old_previous_step_predprefix cfc_a_previous_step_predprefix cfc_b_previous_step_predprefix cfc_c_previous_step_predprefix cfc_d_previous_step_predprefix cfc_new_previous_step_predprefix cfc_quotient_previous_step_predprefix. ((exists cfc_state_previous_step_predprefixprevious. ((exists cfc_left_previous_step_predprefixpreviouscode cfc_right_previous_step_predprefixpreviouscode cfc_matrix_previous_step_predprefixpreviouscode. ((cfc_left_previous_step_predprefixpreviouscode = ((cfc_a_previous_step_predprefix) + (cfc_b_previous_step_predprefix)) * S ((cfc_a_previous_step_predprefix) + (cfc_b_previous_step_predprefix)) + ((cfc_b_previous_step_predprefix) + (cfc_b_previous_step_predprefix))) /\ ((cfc_right_previous_step_predprefixpreviouscode = ((cfc_c_previous_step_predprefix) + (cfc_d_previous_step_predprefix)) * S ((cfc_c_previous_step_predprefix) + (cfc_d_previous_step_predprefix)) + ((cfc_d_previous_step_predprefix) + (cfc_d_previous_step_predprefix))) /\ ((cfc_matrix_previous_step_predprefixpreviouscode = ((cfc_left_previous_step_predprefixpreviouscode) + (cfc_right_previous_step_predprefixpreviouscode)) * S ((cfc_left_previous_step_predprefixpreviouscode) + (cfc_right_previous_step_predprefixpreviouscode)) + ((cfc_right_previous_step_predprefixpreviouscode) + (cfc_right_previous_step_predprefixpreviouscode))) /\ ((cfc_state_previous_step_predprefixprevious) = ((cfc_old_previous_step_predprefix) + (cfc_matrix_previous_step_predprefixpreviouscode)) * S ((cfc_old_previous_step_predprefix) + (cfc_matrix_previous_step_predprefixpreviouscode)) + ((cfc_matrix_previous_step_predprefixpreviouscode) + (cfc_matrix_previous_step_predprefixpreviouscode))))))) /\ (((exists ff_h_previous_step_predprefixpreviousentry. ff_h_previous_step_predprefixpreviousentry + S (cfc_state_previous_step_predprefixprevious) = S ((S (cfc_index_previous_step_predprefix)) * e)) /\ exists ff_q_previous_step_predprefixpreviousentry. h = ff_q_previous_step_predprefixpreviousentry * S ((S (cfc_index_previous_step_predprefix)) * e) + (cfc_state_previous_step_predprefixprevious))))) /\ ((exists cfc_state_previous_step_predprefixfollowing. ((exists cfc_left_previous_step_predprefixfollowingcode cfc_right_previous_step_predprefixfollowingcode cfc_matrix_previous_step_predprefixfollowingcode. ((cfc_left_previous_step_predprefixfollowingcode = (((cfc_quotient_previous_step_predprefix * cfc_a_previous_step_predprefix + cfc_c_previous_step_predprefix)) + ((cfc_quotient_previous_step_predprefix * cfc_b_previous_step_predprefix + cfc_d_previous_step_predprefix))) * S (((cfc_quotient_previous_step_predprefix * cfc_a_previous_step_predprefix + cfc_c_previous_step_predprefix)) + ((cfc_quotient_previous_step_predprefix * cfc_b_previous_step_predprefix + cfc_d_previous_step_predprefix))) + (((cfc_quotient_previous_step_predprefix * cfc_b_previous_step_predprefix + cfc_d_previous_step_predprefix)) + ((cfc_quotient_previous_step_predprefix * cfc_b_previous_step_predprefix + cfc_d_previous_step_predprefix)))) /\ ((cfc_right_previous_step_predprefixfollowingcode = ((cfc_a_previous_step_predprefix) + (cfc_b_previous_step_predprefix)) * S ((cfc_a_previous_step_predprefix) + (cfc_b_previous_step_predprefix)) + ((cfc_b_previous_step_predprefix) + (cfc_b_previous_step_predprefix))) /\ ((cfc_matrix_previous_step_predprefixfollowingcode = ((cfc_left_previous_step_predprefixfollowingcode) + (cfc_right_previous_step_predprefixfollowingcode)) * S ((cfc_left_previous_step_predprefixfollowingcode) + (cfc_right_previous_step_predprefixfollowingcode)) + ((cfc_right_previous_step_predprefixfollowingcode) + (cfc_right_previous_step_predprefixfollowingcode))) /\ ((cfc_state_previous_step_predprefixfollowing) = ((cfc_new_previous_step_predprefix) + (cfc_matrix_previous_step_predprefixfollowingcode)) * S ((cfc_new_previous_step_predprefix) + (cfc_matrix_previous_step_predprefixfollowingcode)) + ((cfc_matrix_previous_step_predprefixfollowingcode) + (cfc_matrix_previous_step_predprefixfollowingcode))))))) /\ (((exists ff_h_previous_step_predprefixfollowingentry. ff_h_previous_step_predprefixfollowingentry + S (cfc_state_previous_step_predprefixfollowing) = S ((S (S cfc_index_previous_step_predprefix)) * e)) /\ exists ff_q_previous_step_predprefixfollowingentry. h = ff_q_previous_step_predprefixfollowingentry * S ((S (S cfc_index_previous_step_predprefix)) * e) + (cfc_state_previous_step_predprefixfollowing))))) /\ (cfc_new_previous_step_predprefix = S ((cfc_quotient_previous_step_predprefix + cfc_old_previous_step_predprefix) * S (cfc_quotient_previous_step_predprefix + cfc_old_previous_step_predprefix) + (cfc_old_previous_step_predprefix + cfc_old_previous_step_predprefix))))))))) /\ ((s = S ((cfc_q_previous_step_pred + cfc_tail_previous_step_pred) * S (cfc_q_previous_step_pred + cfc_tail_previous_step_pred) + (cfc_tail_previous_step_pred + cfc_tail_previous_step_pred))) /\ (((u) = cfc_q_previous_step_pred * cfc_a_previous_step_pred + cfc_c_previous_step_pred) /\ (((U) = cfc_q_previous_step_pred * cfc_b_previous_step_pred + cfc_d_previous_step_pred) /\ (((v) = cfc_a_previous_step_pred) /\ ((V) = cfc_b_previous_step_pred))))))
  97. 0097specialize cf_convergent_matrix_successor_elimination (s)
  98. 0098specialize cf_convergent_matrix_successor_elimination (h)
  99. 0099specialize cf_convergent_matrix_successor_elimination (e)
  100. 0100specialize cf_convergent_matrix_successor_elimination (S k)
  101. 0101specialize cf_convergent_matrix_successor_elimination (u)
  102. 0102specialize cf_convergent_matrix_successor_elimination (U)
  103. 0103specialize cf_convergent_matrix_successor_elimination (v)
  104. 0104specialize cf_convergent_matrix_successor_elimination (V)
  105. 0105apply cf_convergent_matrix_successor_elimination
  106. 0106exact ht
  107. 0107cases hp
  108. 0108cases hp_witness
  109. 0109cases hp_witness_witness
  110. 0110cases hp_witness_witness_witness
  111. 0111cases hp_witness_witness_witness_witness
  112. 0112cases hp_witness_witness_witness_witness_witness
  113. 0113cases hp_witness_witness_witness_witness_witness_witness
  114. 0114cases hp_witness_witness_witness_witness_witness_witness_right
  115. 0115cases hp_witness_witness_witness_witness_witness_witness_right_right
  116. 0116cases hp_witness_witness_witness_witness_witness_witness_right_right_right
  117. 0117cases hp_witness_witness_witness_witness_witness_witness_right_right_right_right
  118. 0118have hi : exists cfc_h_previous_child cfc_e_previous_child cfc_p_previous_child cfc_q_previous_child. exists cfc_tail_previous_childbody. ((exists cfc_state_previous_childbodyinitial. ((exists cfc_left_previous_childbodyinitialcode cfc_right_previous_childbodyinitialcode cfc_matrix_previous_childbodyinitialcode. ((cfc_left_previous_childbodyinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_previous_childbodyinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_previous_childbodyinitialcode = ((cfc_left_previous_childbodyinitialcode) + (cfc_right_previous_childbodyinitialcode)) * S ((cfc_left_previous_childbodyinitialcode) + (cfc_right_previous_childbodyinitialcode)) + ((cfc_right_previous_childbodyinitialcode) + (cfc_right_previous_childbodyinitialcode))) /\ ((cfc_state_previous_childbodyinitial) = ((cfc_tail_previous_childbody) + (cfc_matrix_previous_childbodyinitialcode)) * S ((cfc_tail_previous_childbody) + (cfc_matrix_previous_childbodyinitialcode)) + ((cfc_matrix_previous_childbodyinitialcode) + (cfc_matrix_previous_childbodyinitialcode))))))) /\ (((exists ff_h_previous_childbodyinitialentry. ff_h_previous_childbodyinitialentry + S (cfc_state_previous_childbodyinitial) = S ((S (0)) * cfc_e_previous_child)) /\ exists ff_q_previous_childbodyinitialentry. cfc_h_previous_child = ff_q_previous_childbodyinitialentry * S ((S (0)) * cfc_e_previous_child) + (cfc_state_previous_childbodyinitial))))) /\ ((exists cfc_state_previous_childbodyterminal. ((exists cfc_left_previous_childbodyterminalcode cfc_right_previous_childbodyterminalcode cfc_matrix_previous_childbodyterminalcode. ((cfc_left_previous_childbodyterminalcode = ((x2) + (cfc_p_previous_child)) * S ((x2) + (cfc_p_previous_child)) + ((cfc_p_previous_child) + (cfc_p_previous_child))) /\ ((cfc_right_previous_childbodyterminalcode = ((x4) + (cfc_q_previous_child)) * S ((x4) + (cfc_q_previous_child)) + ((cfc_q_previous_child) + (cfc_q_previous_child))) /\ ((cfc_matrix_previous_childbodyterminalcode = ((cfc_left_previous_childbodyterminalcode) + (cfc_right_previous_childbodyterminalcode)) * S ((cfc_left_previous_childbodyterminalcode) + (cfc_right_previous_childbodyterminalcode)) + ((cfc_right_previous_childbodyterminalcode) + (cfc_right_previous_childbodyterminalcode))) /\ ((cfc_state_previous_childbodyterminal) = ((x) + (cfc_matrix_previous_childbodyterminalcode)) * S ((x) + (cfc_matrix_previous_childbodyterminalcode)) + ((cfc_matrix_previous_childbodyterminalcode) + (cfc_matrix_previous_childbodyterminalcode))))))) /\ (((exists ff_h_previous_childbodyterminalentry. ff_h_previous_childbodyterminalentry + S (cfc_state_previous_childbodyterminal) = S ((S (k)) * cfc_e_previous_child)) /\ exists ff_q_previous_childbodyterminalentry. cfc_h_previous_child = ff_q_previous_childbodyterminalentry * S ((S (k)) * cfc_e_previous_child) + (cfc_state_previous_childbodyterminal))))) /\ (forall cfc_index_previous_childbody. (exists cfba_gap_previous_childbodybound. cfba_gap_previous_childbodybound + S (cfc_index_previous_childbody) = (k)) -> exists cfc_old_previous_childbody cfc_a_previous_childbody cfc_b_previous_childbody cfc_c_previous_childbody cfc_d_previous_childbody cfc_new_previous_childbody cfc_quotient_previous_childbody. ((exists cfc_state_previous_childbodyprevious. ((exists cfc_left_previous_childbodypreviouscode cfc_right_previous_childbodypreviouscode cfc_matrix_previous_childbodypreviouscode. ((cfc_left_previous_childbodypreviouscode = ((cfc_a_previous_childbody) + (cfc_b_previous_childbody)) * S ((cfc_a_previous_childbody) + (cfc_b_previous_childbody)) + ((cfc_b_previous_childbody) + (cfc_b_previous_childbody))) /\ ((cfc_right_previous_childbodypreviouscode = ((cfc_c_previous_childbody) + (cfc_d_previous_childbody)) * S ((cfc_c_previous_childbody) + (cfc_d_previous_childbody)) + ((cfc_d_previous_childbody) + (cfc_d_previous_childbody))) /\ ((cfc_matrix_previous_childbodypreviouscode = ((cfc_left_previous_childbodypreviouscode) + (cfc_right_previous_childbodypreviouscode)) * S ((cfc_left_previous_childbodypreviouscode) + (cfc_right_previous_childbodypreviouscode)) + ((cfc_right_previous_childbodypreviouscode) + (cfc_right_previous_childbodypreviouscode))) /\ ((cfc_state_previous_childbodyprevious) = ((cfc_old_previous_childbody) + (cfc_matrix_previous_childbodypreviouscode)) * S ((cfc_old_previous_childbody) + (cfc_matrix_previous_childbodypreviouscode)) + ((cfc_matrix_previous_childbodypreviouscode) + (cfc_matrix_previous_childbodypreviouscode))))))) /\ (((exists ff_h_previous_childbodypreviousentry. ff_h_previous_childbodypreviousentry + S (cfc_state_previous_childbodyprevious) = S ((S (cfc_index_previous_childbody)) * cfc_e_previous_child)) /\ exists ff_q_previous_childbodypreviousentry. cfc_h_previous_child = ff_q_previous_childbodypreviousentry * S ((S (cfc_index_previous_childbody)) * cfc_e_previous_child) + (cfc_state_previous_childbodyprevious))))) /\ ((exists cfc_state_previous_childbodyfollowing. ((exists cfc_left_previous_childbodyfollowingcode cfc_right_previous_childbodyfollowingcode cfc_matrix_previous_childbodyfollowingcode. ((cfc_left_previous_childbodyfollowingcode = (((cfc_quotient_previous_childbody * cfc_a_previous_childbody + cfc_c_previous_childbody)) + ((cfc_quotient_previous_childbody * cfc_b_previous_childbody + cfc_d_previous_childbody))) * S (((cfc_quotient_previous_childbody * cfc_a_previous_childbody + cfc_c_previous_childbody)) + ((cfc_quotient_previous_childbody * cfc_b_previous_childbody + cfc_d_previous_childbody))) + (((cfc_quotient_previous_childbody * cfc_b_previous_childbody + cfc_d_previous_childbody)) + ((cfc_quotient_previous_childbody * cfc_b_previous_childbody + cfc_d_previous_childbody)))) /\ ((cfc_right_previous_childbodyfollowingcode = ((cfc_a_previous_childbody) + (cfc_b_previous_childbody)) * S ((cfc_a_previous_childbody) + (cfc_b_previous_childbody)) + ((cfc_b_previous_childbody) + (cfc_b_previous_childbody))) /\ ((cfc_matrix_previous_childbodyfollowingcode = ((cfc_left_previous_childbodyfollowingcode) + (cfc_right_previous_childbodyfollowingcode)) * S ((cfc_left_previous_childbodyfollowingcode) + (cfc_right_previous_childbodyfollowingcode)) + ((cfc_right_previous_childbodyfollowingcode) + (cfc_right_previous_childbodyfollowingcode))) /\ ((cfc_state_previous_childbodyfollowing) = ((cfc_new_previous_childbody) + (cfc_matrix_previous_childbodyfollowingcode)) * S ((cfc_new_previous_childbody) + (cfc_matrix_previous_childbodyfollowingcode)) + ((cfc_matrix_previous_childbodyfollowingcode) + (cfc_matrix_previous_childbodyfollowingcode))))))) /\ (((exists ff_h_previous_childbodyfollowingentry. ff_h_previous_childbodyfollowingentry + S (cfc_state_previous_childbodyfollowing) = S ((S (S cfc_index_previous_childbody)) * cfc_e_previous_child)) /\ exists ff_q_previous_childbodyfollowingentry. cfc_h_previous_child = ff_q_previous_childbodyfollowingentry * S ((S (S cfc_index_previous_childbody)) * cfc_e_previous_child) + (cfc_state_previous_childbodyfollowing))))) /\ (cfc_new_previous_childbody = S ((cfc_quotient_previous_childbody + cfc_old_previous_childbody) * S (cfc_quotient_previous_childbody + cfc_old_previous_childbody) + (cfc_old_previous_childbody + cfc_old_previous_childbody))))))))
  119. 0119specialize IH (x)
  120. 0120specialize IH (h)
  121. 0121specialize IH (e)
  122. 0122specialize IH (x1)
  123. 0123specialize IH (x2)
  124. 0124specialize IH (x3)
  125. 0125specialize IH (x4)
  126. 0126apply IH
  127. 0127exact hp_witness_witness_witness_witness_witness_witness_left
  128. 0128cases hi
  129. 0129cases hi_witness
  130. 0130cases hi_witness_witness
  131. 0131cases hi_witness_witness_witness
  132. 0132have hext : exists H E. exists cfc_tail_previous_extension. ((exists cfc_state_previous_extensioninitial. ((exists cfc_left_previous_extensioninitialcode cfc_right_previous_extensioninitialcode cfc_matrix_previous_extensioninitialcode. ((cfc_left_previous_extensioninitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_previous_extensioninitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_previous_extensioninitialcode = ((cfc_left_previous_extensioninitialcode) + (cfc_right_previous_extensioninitialcode)) * S ((cfc_left_previous_extensioninitialcode) + (cfc_right_previous_extensioninitialcode)) + ((cfc_right_previous_extensioninitialcode) + (cfc_right_previous_extensioninitialcode))) /\ ((cfc_state_previous_extensioninitial) = ((cfc_tail_previous_extension) + (cfc_matrix_previous_extensioninitialcode)) * S ((cfc_tail_previous_extension) + (cfc_matrix_previous_extensioninitialcode)) + ((cfc_matrix_previous_extensioninitialcode) + (cfc_matrix_previous_extensioninitialcode))))))) /\ (((exists ff_h_previous_extensioninitialentry. ff_h_previous_extensioninitialentry + S (cfc_state_previous_extensioninitial) = S ((S (0)) * E)) /\ exists ff_q_previous_extensioninitialentry. H = ff_q_previous_extensioninitialentry * S ((S (0)) * E) + (cfc_state_previous_extensioninitial))))) /\ ((exists cfc_state_previous_extensionterminal. ((exists cfc_left_previous_extensionterminalcode cfc_right_previous_extensionterminalcode cfc_matrix_previous_extensionterminalcode. ((cfc_left_previous_extensionterminalcode = (((x5 * x2 + x4)) + ((x5 * x8 + x9))) * S (((x5 * x2 + x4)) + ((x5 * x8 + x9))) + (((x5 * x8 + x9)) + ((x5 * x8 + x9)))) /\ ((cfc_right_previous_extensionterminalcode = ((x2) + (x8)) * S ((x2) + (x8)) + ((x8) + (x8))) /\ ((cfc_matrix_previous_extensionterminalcode = ((cfc_left_previous_extensionterminalcode) + (cfc_right_previous_extensionterminalcode)) * S ((cfc_left_previous_extensionterminalcode) + (cfc_right_previous_extensionterminalcode)) + ((cfc_right_previous_extensionterminalcode) + (cfc_right_previous_extensionterminalcode))) /\ ((cfc_state_previous_extensionterminal) = ((s) + (cfc_matrix_previous_extensionterminalcode)) * S ((s) + (cfc_matrix_previous_extensionterminalcode)) + ((cfc_matrix_previous_extensionterminalcode) + (cfc_matrix_previous_extensionterminalcode))))))) /\ (((exists ff_h_previous_extensionterminalentry. ff_h_previous_extensionterminalentry + S (cfc_state_previous_extensionterminal) = S ((S (S k)) * E)) /\ exists ff_q_previous_extensionterminalentry. H = ff_q_previous_extensionterminalentry * S ((S (S k)) * E) + (cfc_state_previous_extensionterminal))))) /\ (forall cfc_index_previous_extension. (exists cfba_gap_previous_extensionbound. cfba_gap_previous_extensionbound + S (cfc_index_previous_extension) = (S k)) -> exists cfc_old_previous_extension cfc_a_previous_extension cfc_b_previous_extension cfc_c_previous_extension cfc_d_previous_extension cfc_new_previous_extension cfc_quotient_previous_extension. ((exists cfc_state_previous_extensionprevious. ((exists cfc_left_previous_extensionpreviouscode cfc_right_previous_extensionpreviouscode cfc_matrix_previous_extensionpreviouscode. ((cfc_left_previous_extensionpreviouscode = ((cfc_a_previous_extension) + (cfc_b_previous_extension)) * S ((cfc_a_previous_extension) + (cfc_b_previous_extension)) + ((cfc_b_previous_extension) + (cfc_b_previous_extension))) /\ ((cfc_right_previous_extensionpreviouscode = ((cfc_c_previous_extension) + (cfc_d_previous_extension)) * S ((cfc_c_previous_extension) + (cfc_d_previous_extension)) + ((cfc_d_previous_extension) + (cfc_d_previous_extension))) /\ ((cfc_matrix_previous_extensionpreviouscode = ((cfc_left_previous_extensionpreviouscode) + (cfc_right_previous_extensionpreviouscode)) * S ((cfc_left_previous_extensionpreviouscode) + (cfc_right_previous_extensionpreviouscode)) + ((cfc_right_previous_extensionpreviouscode) + (cfc_right_previous_extensionpreviouscode))) /\ ((cfc_state_previous_extensionprevious) = ((cfc_old_previous_extension) + (cfc_matrix_previous_extensionpreviouscode)) * S ((cfc_old_previous_extension) + (cfc_matrix_previous_extensionpreviouscode)) + ((cfc_matrix_previous_extensionpreviouscode) + (cfc_matrix_previous_extensionpreviouscode))))))) /\ (((exists ff_h_previous_extensionpreviousentry. ff_h_previous_extensionpreviousentry + S (cfc_state_previous_extensionprevious) = S ((S (cfc_index_previous_extension)) * E)) /\ exists ff_q_previous_extensionpreviousentry. H = ff_q_previous_extensionpreviousentry * S ((S (cfc_index_previous_extension)) * E) + (cfc_state_previous_extensionprevious))))) /\ ((exists cfc_state_previous_extensionfollowing. ((exists cfc_left_previous_extensionfollowingcode cfc_right_previous_extensionfollowingcode cfc_matrix_previous_extensionfollowingcode. ((cfc_left_previous_extensionfollowingcode = (((cfc_quotient_previous_extension * cfc_a_previous_extension + cfc_c_previous_extension)) + ((cfc_quotient_previous_extension * cfc_b_previous_extension + cfc_d_previous_extension))) * S (((cfc_quotient_previous_extension * cfc_a_previous_extension + cfc_c_previous_extension)) + ((cfc_quotient_previous_extension * cfc_b_previous_extension + cfc_d_previous_extension))) + (((cfc_quotient_previous_extension * cfc_b_previous_extension + cfc_d_previous_extension)) + ((cfc_quotient_previous_extension * cfc_b_previous_extension + cfc_d_previous_extension)))) /\ ((cfc_right_previous_extensionfollowingcode = ((cfc_a_previous_extension) + (cfc_b_previous_extension)) * S ((cfc_a_previous_extension) + (cfc_b_previous_extension)) + ((cfc_b_previous_extension) + (cfc_b_previous_extension))) /\ ((cfc_matrix_previous_extensionfollowingcode = ((cfc_left_previous_extensionfollowingcode) + (cfc_right_previous_extensionfollowingcode)) * S ((cfc_left_previous_extensionfollowingcode) + (cfc_right_previous_extensionfollowingcode)) + ((cfc_right_previous_extensionfollowingcode) + (cfc_right_previous_extensionfollowingcode))) /\ ((cfc_state_previous_extensionfollowing) = ((cfc_new_previous_extension) + (cfc_matrix_previous_extensionfollowingcode)) * S ((cfc_new_previous_extension) + (cfc_matrix_previous_extensionfollowingcode)) + ((cfc_matrix_previous_extensionfollowingcode) + (cfc_matrix_previous_extensionfollowingcode))))))) /\ (((exists ff_h_previous_extensionfollowingentry. ff_h_previous_extensionfollowingentry + S (cfc_state_previous_extensionfollowing) = S ((S (S cfc_index_previous_extension)) * E)) /\ exists ff_q_previous_extensionfollowingentry. H = ff_q_previous_extensionfollowingentry * S ((S (S cfc_index_previous_extension)) * E) + (cfc_state_previous_extensionfollowing))))) /\ (cfc_new_previous_extension = S ((cfc_quotient_previous_extension + cfc_old_previous_extension) * S (cfc_quotient_previous_extension + cfc_old_previous_extension) + (cfc_old_previous_extension + cfc_old_previous_extension))))))))
  133. 0133specialize cf_convergent_matrix_prepend_exists (x)
  134. 0134specialize cf_convergent_matrix_prepend_exists (x6)
  135. 0135specialize cf_convergent_matrix_prepend_exists (x7)
  136. 0136specialize cf_convergent_matrix_prepend_exists (k)
  137. 0137specialize cf_convergent_matrix_prepend_exists (x2)
  138. 0138specialize cf_convergent_matrix_prepend_exists (x8)
  139. 0139specialize cf_convergent_matrix_prepend_exists (x4)
  140. 0140specialize cf_convergent_matrix_prepend_exists (x9)
  141. 0141specialize cf_convergent_matrix_prepend_exists (x5)
  142. 0142specialize cf_convergent_matrix_prepend_exists (s)
  143. 0143apply cf_convergent_matrix_prepend_exists
  144. 0144exact hi_witness_witness_witness_witness
  145. 0145exact hp_witness_witness_witness_witness_witness_witness_right_left
  146. 0146cases hext
  147. 0147cases hext_witness
  148. 0148exists x10
  149. 0149exists x11
  150. 0150exists x5 * x8 + x9
  151. 0151exists x8
  152. 0152specialize cf_convergent_matrix_entry_transport (s)
  153. 0153specialize cf_convergent_matrix_entry_transport (x10)
  154. 0154specialize cf_convergent_matrix_entry_transport (x11)
  155. 0155specialize cf_convergent_matrix_entry_transport (S k)
  156. 0156specialize cf_convergent_matrix_entry_transport (U)
  157. 0157specialize cf_convergent_matrix_entry_transport (x5 * x8 + x9)
  158. 0158specialize cf_convergent_matrix_entry_transport (V)
  159. 0159specialize cf_convergent_matrix_entry_transport (x8)
  160. 0160specialize cf_convergent_matrix_entry_transport ((x5 * x2 + x4))
  161. 0161specialize cf_convergent_matrix_entry_transport ((x5 * x8 + x9))
  162. 0162specialize cf_convergent_matrix_entry_transport (x2)
  163. 0163specialize cf_convergent_matrix_entry_transport (x8)
  164. 0164apply cf_convergent_matrix_entry_transport
  165. 0165exact hp_witness_witness_witness_witness_witness_witness_right_right_right_left
  166. 0166refl
  167. 0167exact hp_witness_witness_witness_witness_witness_witness_right_right_right_right_right
  168. 0168refl
  169. 0169exact hext_witness_witness