BA004F

cf_convergent_second_column_is_previous_prefix

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.

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

The initial 0/1 convergent is included: u is natural, not necessarily positive. Comparison denominators are strictly smaller and positive. Signed competitors are represented by an arbitrary difference rp−rn. Approximation inequalities are proved from the trace, never stored as assumptions in Convergent.

Exact theorem in conservative defined notation

∀ k. ∀ s. ∀ h. ∀ e. ∀ u. ∀ U. ∀ v. ∀ V. ConvergentMatrixTrace(s,h,e,S k,u,U,v,V) → ∃ x. ∃ y. ∃ z. ∃ n. ConvergentMatrixTrace(s,x,y,k,U,z,V,n)

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

Definition DAG

ListCell(s,q,t) · 2ConvergentMatrixTrace(s,h,e,k,u,U,v,V) · 8

Actual proof prerequisites

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

Complete tactic proof in conservative notation

All 169 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (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
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: 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)Original native command in the exact edition
  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(s,H,E,1,x5,1,1,0)Original native command in the exact edition
  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(s,H,E,0,1,0,0,1)Original native command in the exact edition
  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: 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)Original native command in the exact edition
  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(x,cfc_h_previous_child,cfc_e_previous_child,k,x2,cfc_p_previous_child,x4,cfc_q_previous_child)Original native command in the exact edition
  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(s,H,E,S k,x5 · x2 + x4,x5 · x8 + x9,x2,x8)Original native command in the exact edition
  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 defined 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 : ∃ 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))))
  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 : ∃ H. ∃ E. ConvergentMatrixTrace(s,H,E,1,x5,1,1,0)
  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 : ∃ H. ∃ E. ConvergentMatrixTrace(s,H,E,0,1,0,0,1)
  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 : ∃ 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))))
  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 : ∃ 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)
  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 : ∃ H. ∃ E. ConvergentMatrixTrace(s,H,E,S k,x5 · x2 + x4,x5 · x8 + x9,x2,x8)
  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