BA0034

cf_convergent_matrix_nonempty_list

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

A nonempty convergent prefix must consume an actual tagged quotient cell; nil cannot be mistaken for an initial convergent.

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

Exact expanded first-order arithmetic statement

forall s h e k u U v V. (exists cfc_tail_matrix_nonempty. ((exists cfc_state_matrix_nonemptyinitial. ((exists cfc_left_matrix_nonemptyinitialcode cfc_right_matrix_nonemptyinitialcode cfc_matrix_matrix_nonemptyinitialcode. ((cfc_left_matrix_nonemptyinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_matrix_nonemptyinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_matrix_nonemptyinitialcode = ((cfc_left_matrix_nonemptyinitialcode) + (cfc_right_matrix_nonemptyinitialcode)) * S ((cfc_left_matrix_nonemptyinitialcode) + (cfc_right_matrix_nonemptyinitialcode)) + ((cfc_right_matrix_nonemptyinitialcode) + (cfc_right_matrix_nonemptyinitialcode))) /\ ((cfc_state_matrix_nonemptyinitial) = ((cfc_tail_matrix_nonempty) + (cfc_matrix_matrix_nonemptyinitialcode)) * S ((cfc_tail_matrix_nonempty) + (cfc_matrix_matrix_nonemptyinitialcode)) + ((cfc_matrix_matrix_nonemptyinitialcode) + (cfc_matrix_matrix_nonemptyinitialcode))))))) /\ (((exists ff_h_matrix_nonemptyinitialentry. ff_h_matrix_nonemptyinitialentry + S (cfc_state_matrix_nonemptyinitial) = S ((S (0)) * e)) /\ exists ff_q_matrix_nonemptyinitialentry. h = ff_q_matrix_nonemptyinitialentry * S ((S (0)) * e) + (cfc_state_matrix_nonemptyinitial))))) /\ ((exists cfc_state_matrix_nonemptyterminal. ((exists cfc_left_matrix_nonemptyterminalcode cfc_right_matrix_nonemptyterminalcode cfc_matrix_matrix_nonemptyterminalcode. ((cfc_left_matrix_nonemptyterminalcode = ((u) + (U)) * S ((u) + (U)) + ((U) + (U))) /\ ((cfc_right_matrix_nonemptyterminalcode = ((v) + (V)) * S ((v) + (V)) + ((V) + (V))) /\ ((cfc_matrix_matrix_nonemptyterminalcode = ((cfc_left_matrix_nonemptyterminalcode) + (cfc_right_matrix_nonemptyterminalcode)) * S ((cfc_left_matrix_nonemptyterminalcode) + (cfc_right_matrix_nonemptyterminalcode)) + ((cfc_right_matrix_nonemptyterminalcode) + (cfc_right_matrix_nonemptyterminalcode))) /\ ((cfc_state_matrix_nonemptyterminal) = ((s) + (cfc_matrix_matrix_nonemptyterminalcode)) * S ((s) + (cfc_matrix_matrix_nonemptyterminalcode)) + ((cfc_matrix_matrix_nonemptyterminalcode) + (cfc_matrix_matrix_nonemptyterminalcode))))))) /\ (((exists ff_h_matrix_nonemptyterminalentry. ff_h_matrix_nonemptyterminalentry + S (cfc_state_matrix_nonemptyterminal) = S ((S (S k)) * e)) /\ exists ff_q_matrix_nonemptyterminalentry. h = ff_q_matrix_nonemptyterminalentry * S ((S (S k)) * e) + (cfc_state_matrix_nonemptyterminal))))) /\ (forall cfc_index_matrix_nonempty. (exists cfba_gap_matrix_nonemptybound. cfba_gap_matrix_nonemptybound + S (cfc_index_matrix_nonempty) = (S k)) -> exists cfc_old_matrix_nonempty cfc_a_matrix_nonempty cfc_b_matrix_nonempty cfc_c_matrix_nonempty cfc_d_matrix_nonempty cfc_new_matrix_nonempty cfc_quotient_matrix_nonempty. ((exists cfc_state_matrix_nonemptyprevious. ((exists cfc_left_matrix_nonemptypreviouscode cfc_right_matrix_nonemptypreviouscode cfc_matrix_matrix_nonemptypreviouscode. ((cfc_left_matrix_nonemptypreviouscode = ((cfc_a_matrix_nonempty) + (cfc_b_matrix_nonempty)) * S ((cfc_a_matrix_nonempty) + (cfc_b_matrix_nonempty)) + ((cfc_b_matrix_nonempty) + (cfc_b_matrix_nonempty))) /\ ((cfc_right_matrix_nonemptypreviouscode = ((cfc_c_matrix_nonempty) + (cfc_d_matrix_nonempty)) * S ((cfc_c_matrix_nonempty) + (cfc_d_matrix_nonempty)) + ((cfc_d_matrix_nonempty) + (cfc_d_matrix_nonempty))) /\ ((cfc_matrix_matrix_nonemptypreviouscode = ((cfc_left_matrix_nonemptypreviouscode) + (cfc_right_matrix_nonemptypreviouscode)) * S ((cfc_left_matrix_nonemptypreviouscode) + (cfc_right_matrix_nonemptypreviouscode)) + ((cfc_right_matrix_nonemptypreviouscode) + (cfc_right_matrix_nonemptypreviouscode))) /\ ((cfc_state_matrix_nonemptyprevious) = ((cfc_old_matrix_nonempty) + (cfc_matrix_matrix_nonemptypreviouscode)) * S ((cfc_old_matrix_nonempty) + (cfc_matrix_matrix_nonemptypreviouscode)) + ((cfc_matrix_matrix_nonemptypreviouscode) + (cfc_matrix_matrix_nonemptypreviouscode))))))) /\ (((exists ff_h_matrix_nonemptypreviousentry. ff_h_matrix_nonemptypreviousentry + S (cfc_state_matrix_nonemptyprevious) = S ((S (cfc_index_matrix_nonempty)) * e)) /\ exists ff_q_matrix_nonemptypreviousentry. h = ff_q_matrix_nonemptypreviousentry * S ((S (cfc_index_matrix_nonempty)) * e) + (cfc_state_matrix_nonemptyprevious))))) /\ ((exists cfc_state_matrix_nonemptyfollowing. ((exists cfc_left_matrix_nonemptyfollowingcode cfc_right_matrix_nonemptyfollowingcode cfc_matrix_matrix_nonemptyfollowingcode. ((cfc_left_matrix_nonemptyfollowingcode = (((cfc_quotient_matrix_nonempty * cfc_a_matrix_nonempty + cfc_c_matrix_nonempty)) + ((cfc_quotient_matrix_nonempty * cfc_b_matrix_nonempty + cfc_d_matrix_nonempty))) * S (((cfc_quotient_matrix_nonempty * cfc_a_matrix_nonempty + cfc_c_matrix_nonempty)) + ((cfc_quotient_matrix_nonempty * cfc_b_matrix_nonempty + cfc_d_matrix_nonempty))) + (((cfc_quotient_matrix_nonempty * cfc_b_matrix_nonempty + cfc_d_matrix_nonempty)) + ((cfc_quotient_matrix_nonempty * cfc_b_matrix_nonempty + cfc_d_matrix_nonempty)))) /\ ((cfc_right_matrix_nonemptyfollowingcode = ((cfc_a_matrix_nonempty) + (cfc_b_matrix_nonempty)) * S ((cfc_a_matrix_nonempty) + (cfc_b_matrix_nonempty)) + ((cfc_b_matrix_nonempty) + (cfc_b_matrix_nonempty))) /\ ((cfc_matrix_matrix_nonemptyfollowingcode = ((cfc_left_matrix_nonemptyfollowingcode) + (cfc_right_matrix_nonemptyfollowingcode)) * S ((cfc_left_matrix_nonemptyfollowingcode) + (cfc_right_matrix_nonemptyfollowingcode)) + ((cfc_right_matrix_nonemptyfollowingcode) + (cfc_right_matrix_nonemptyfollowingcode))) /\ ((cfc_state_matrix_nonemptyfollowing) = ((cfc_new_matrix_nonempty) + (cfc_matrix_matrix_nonemptyfollowingcode)) * S ((cfc_new_matrix_nonempty) + (cfc_matrix_matrix_nonemptyfollowingcode)) + ((cfc_matrix_matrix_nonemptyfollowingcode) + (cfc_matrix_matrix_nonemptyfollowingcode))))))) /\ (((exists ff_h_matrix_nonemptyfollowingentry. ff_h_matrix_nonemptyfollowingentry + S (cfc_state_matrix_nonemptyfollowing) = S ((S (S cfc_index_matrix_nonempty)) * e)) /\ exists ff_q_matrix_nonemptyfollowingentry. h = ff_q_matrix_nonemptyfollowingentry * S ((S (S cfc_index_matrix_nonempty)) * e) + (cfc_state_matrix_nonemptyfollowing))))) /\ (cfc_new_matrix_nonempty = S ((cfc_quotient_matrix_nonempty + cfc_old_matrix_nonempty) * S (cfc_quotient_matrix_nonempty + cfc_old_matrix_nonempty) + (cfc_old_matrix_nonempty + cfc_old_matrix_nonempty))))))))) -> ~(s = 0)

Constructive proof overview

Generated structural guide

A nonempty convergent prefix must consume an actual tagged quotient cell; nil cannot be mistaken for an initial convergent.

The unchanged tactic script uses 2 declared prerequisites and contains 38 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 cell_nonzero Alpha theorem; checked-use authorized

Direct dependents

BA003D cf_convergent_euclidean_matrix_step_alignment

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

38 script commands · 6 reading checkpoints · 1 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (1)
cf convergent matrix successor elimination

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.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro s
  2. L2
    intro h
  3. L3
    intro e
  4. L4
    intro k
  5. L5
    intro u
  6. L6
    intro U
  7. L7
    intro v
  8. L8
    intro V
  9. L9
    intro ht
  10. L10
    intro hz
02Establish hpL11–20

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

  1. L11
    have hp · expand full local formula (686 characters)have hp : ∃ cfc_tail_matrix_nonempty_pred. ∃ cfc_a_matrix_nonempty_pred. ∃ cfc_b_matrix_nonempty_pred. ∃ cfc_c_matrix_nonempty_pred. ∃ cfc_d_matrix_nonempty_pred. ∃ cfc_q_matrix_nonempty_pred. ConvergentMatrixTrace(cfc_tail_matrix_nonempty_pred,h,e,k,cfc_a_matrix_nonempty_pred,cfc_b_matrix_nonempty_pred,cfc_c_matrix_nonempty_pred,cfc_d_matrix_nonempty_pred) ∧ (ListCell(s,cfc_q_matrix_nonempty_pred,cfc_tail_matrix_nonempty_pred) ∧ (u = cfc_q_matrix_nonempty_pred · cfc_a_matrix_nonempty_pred + cfc_c_matrix_nonempty_pred ∧ (U = cfc_q_matrix_nonempty_pred · cfc_b_matrix_nonempty_pred + cfc_d_matrix_nonempty_pred ∧ (v = cfc_a_matrix_nonempty_pred ∧ V = cfc_b_matrix_nonempty_pred))))
    Definitions: ListCellConvergentMatrixTrace
  2. L12
    specialize cf_convergent_matrix_successor_elimination (s)
  3. L13
    specialize cf_convergent_matrix_successor_elimination (h)
  4. L14
    specialize cf_convergent_matrix_successor_elimination (e)
  5. L15
    specialize cf_convergent_matrix_successor_elimination (k)
  6. L16
    specialize cf_convergent_matrix_successor_elimination (u)
  7. L17
    specialize cf_convergent_matrix_successor_elimination (U)
  8. L18
    specialize cf_convergent_matrix_successor_elimination (v)
  9. L19
    specialize cf_convergent_matrix_successor_elimination (V)
  10. L20
    apply cf_convergent_matrix_successor_elimination
03Use earlier factsL21–21

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

  1. L21
    exact ht
04Separate the logical casesL22–31

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

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

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

  1. L32
    cases hp_witness_witness_witness_witness_witness_witness_right_right_right_right
06Use earlier factsL33–38

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

  1. L33
    specialize cell_nonzero (s)
  2. L34
    specialize cell_nonzero (x5)
  3. L35
    specialize cell_nonzero (x)
  4. L36
    apply cell_nonzero
  5. L37
    exact hp_witness_witness_witness_witness_witness_witness_right_left
  6. L38
    exact hz

Library-wide reading audit

Original exact command ledger · 38 lines
  1. 0001intro s
  2. 0002intro h
  3. 0003intro e
  4. 0004intro k
  5. 0005intro u
  6. 0006intro U
  7. 0007intro v
  8. 0008intro V
  9. 0009intro ht
  10. 0010intro hz
  11. 0011have hp : exists cfc_tail_matrix_nonempty_pred cfc_a_matrix_nonempty_pred cfc_b_matrix_nonempty_pred cfc_c_matrix_nonempty_pred cfc_d_matrix_nonempty_pred cfc_q_matrix_nonempty_pred. ((exists cfc_tail_matrix_nonempty_predprefix. ((exists cfc_state_matrix_nonempty_predprefixinitial. ((exists cfc_left_matrix_nonempty_predprefixinitialcode cfc_right_matrix_nonempty_predprefixinitialcode cfc_matrix_matrix_nonempty_predprefixinitialcode. ((cfc_left_matrix_nonempty_predprefixinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_matrix_nonempty_predprefixinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_matrix_nonempty_predprefixinitialcode = ((cfc_left_matrix_nonempty_predprefixinitialcode) + (cfc_right_matrix_nonempty_predprefixinitialcode)) * S ((cfc_left_matrix_nonempty_predprefixinitialcode) + (cfc_right_matrix_nonempty_predprefixinitialcode)) + ((cfc_right_matrix_nonempty_predprefixinitialcode) + (cfc_right_matrix_nonempty_predprefixinitialcode))) /\ ((cfc_state_matrix_nonempty_predprefixinitial) = ((cfc_tail_matrix_nonempty_predprefix) + (cfc_matrix_matrix_nonempty_predprefixinitialcode)) * S ((cfc_tail_matrix_nonempty_predprefix) + (cfc_matrix_matrix_nonempty_predprefixinitialcode)) + ((cfc_matrix_matrix_nonempty_predprefixinitialcode) + (cfc_matrix_matrix_nonempty_predprefixinitialcode))))))) /\ (((exists ff_h_matrix_nonempty_predprefixinitialentry. ff_h_matrix_nonempty_predprefixinitialentry + S (cfc_state_matrix_nonempty_predprefixinitial) = S ((S (0)) * e)) /\ exists ff_q_matrix_nonempty_predprefixinitialentry. h = ff_q_matrix_nonempty_predprefixinitialentry * S ((S (0)) * e) + (cfc_state_matrix_nonempty_predprefixinitial))))) /\ ((exists cfc_state_matrix_nonempty_predprefixterminal. ((exists cfc_left_matrix_nonempty_predprefixterminalcode cfc_right_matrix_nonempty_predprefixterminalcode cfc_matrix_matrix_nonempty_predprefixterminalcode. ((cfc_left_matrix_nonempty_predprefixterminalcode = ((cfc_a_matrix_nonempty_pred) + (cfc_b_matrix_nonempty_pred)) * S ((cfc_a_matrix_nonempty_pred) + (cfc_b_matrix_nonempty_pred)) + ((cfc_b_matrix_nonempty_pred) + (cfc_b_matrix_nonempty_pred))) /\ ((cfc_right_matrix_nonempty_predprefixterminalcode = ((cfc_c_matrix_nonempty_pred) + (cfc_d_matrix_nonempty_pred)) * S ((cfc_c_matrix_nonempty_pred) + (cfc_d_matrix_nonempty_pred)) + ((cfc_d_matrix_nonempty_pred) + (cfc_d_matrix_nonempty_pred))) /\ ((cfc_matrix_matrix_nonempty_predprefixterminalcode = ((cfc_left_matrix_nonempty_predprefixterminalcode) + (cfc_right_matrix_nonempty_predprefixterminalcode)) * S ((cfc_left_matrix_nonempty_predprefixterminalcode) + (cfc_right_matrix_nonempty_predprefixterminalcode)) + ((cfc_right_matrix_nonempty_predprefixterminalcode) + (cfc_right_matrix_nonempty_predprefixterminalcode))) /\ ((cfc_state_matrix_nonempty_predprefixterminal) = ((cfc_tail_matrix_nonempty_pred) + (cfc_matrix_matrix_nonempty_predprefixterminalcode)) * S ((cfc_tail_matrix_nonempty_pred) + (cfc_matrix_matrix_nonempty_predprefixterminalcode)) + ((cfc_matrix_matrix_nonempty_predprefixterminalcode) + (cfc_matrix_matrix_nonempty_predprefixterminalcode))))))) /\ (((exists ff_h_matrix_nonempty_predprefixterminalentry. ff_h_matrix_nonempty_predprefixterminalentry + S (cfc_state_matrix_nonempty_predprefixterminal) = S ((S (k)) * e)) /\ exists ff_q_matrix_nonempty_predprefixterminalentry. h = ff_q_matrix_nonempty_predprefixterminalentry * S ((S (k)) * e) + (cfc_state_matrix_nonempty_predprefixterminal))))) /\ (forall cfc_index_matrix_nonempty_predprefix. (exists cfba_gap_matrix_nonempty_predprefixbound. cfba_gap_matrix_nonempty_predprefixbound + S (cfc_index_matrix_nonempty_predprefix) = (k)) -> exists cfc_old_matrix_nonempty_predprefix cfc_a_matrix_nonempty_predprefix cfc_b_matrix_nonempty_predprefix cfc_c_matrix_nonempty_predprefix cfc_d_matrix_nonempty_predprefix cfc_new_matrix_nonempty_predprefix cfc_quotient_matrix_nonempty_predprefix. ((exists cfc_state_matrix_nonempty_predprefixprevious. ((exists cfc_left_matrix_nonempty_predprefixpreviouscode cfc_right_matrix_nonempty_predprefixpreviouscode cfc_matrix_matrix_nonempty_predprefixpreviouscode. ((cfc_left_matrix_nonempty_predprefixpreviouscode = ((cfc_a_matrix_nonempty_predprefix) + (cfc_b_matrix_nonempty_predprefix)) * S ((cfc_a_matrix_nonempty_predprefix) + (cfc_b_matrix_nonempty_predprefix)) + ((cfc_b_matrix_nonempty_predprefix) + (cfc_b_matrix_nonempty_predprefix))) /\ ((cfc_right_matrix_nonempty_predprefixpreviouscode = ((cfc_c_matrix_nonempty_predprefix) + (cfc_d_matrix_nonempty_predprefix)) * S ((cfc_c_matrix_nonempty_predprefix) + (cfc_d_matrix_nonempty_predprefix)) + ((cfc_d_matrix_nonempty_predprefix) + (cfc_d_matrix_nonempty_predprefix))) /\ ((cfc_matrix_matrix_nonempty_predprefixpreviouscode = ((cfc_left_matrix_nonempty_predprefixpreviouscode) + (cfc_right_matrix_nonempty_predprefixpreviouscode)) * S ((cfc_left_matrix_nonempty_predprefixpreviouscode) + (cfc_right_matrix_nonempty_predprefixpreviouscode)) + ((cfc_right_matrix_nonempty_predprefixpreviouscode) + (cfc_right_matrix_nonempty_predprefixpreviouscode))) /\ ((cfc_state_matrix_nonempty_predprefixprevious) = ((cfc_old_matrix_nonempty_predprefix) + (cfc_matrix_matrix_nonempty_predprefixpreviouscode)) * S ((cfc_old_matrix_nonempty_predprefix) + (cfc_matrix_matrix_nonempty_predprefixpreviouscode)) + ((cfc_matrix_matrix_nonempty_predprefixpreviouscode) + (cfc_matrix_matrix_nonempty_predprefixpreviouscode))))))) /\ (((exists ff_h_matrix_nonempty_predprefixpreviousentry. ff_h_matrix_nonempty_predprefixpreviousentry + S (cfc_state_matrix_nonempty_predprefixprevious) = S ((S (cfc_index_matrix_nonempty_predprefix)) * e)) /\ exists ff_q_matrix_nonempty_predprefixpreviousentry. h = ff_q_matrix_nonempty_predprefixpreviousentry * S ((S (cfc_index_matrix_nonempty_predprefix)) * e) + (cfc_state_matrix_nonempty_predprefixprevious))))) /\ ((exists cfc_state_matrix_nonempty_predprefixfollowing. ((exists cfc_left_matrix_nonempty_predprefixfollowingcode cfc_right_matrix_nonempty_predprefixfollowingcode cfc_matrix_matrix_nonempty_predprefixfollowingcode. ((cfc_left_matrix_nonempty_predprefixfollowingcode = (((cfc_quotient_matrix_nonempty_predprefix * cfc_a_matrix_nonempty_predprefix + cfc_c_matrix_nonempty_predprefix)) + ((cfc_quotient_matrix_nonempty_predprefix * cfc_b_matrix_nonempty_predprefix + cfc_d_matrix_nonempty_predprefix))) * S (((cfc_quotient_matrix_nonempty_predprefix * cfc_a_matrix_nonempty_predprefix + cfc_c_matrix_nonempty_predprefix)) + ((cfc_quotient_matrix_nonempty_predprefix * cfc_b_matrix_nonempty_predprefix + cfc_d_matrix_nonempty_predprefix))) + (((cfc_quotient_matrix_nonempty_predprefix * cfc_b_matrix_nonempty_predprefix + cfc_d_matrix_nonempty_predprefix)) + ((cfc_quotient_matrix_nonempty_predprefix * cfc_b_matrix_nonempty_predprefix + cfc_d_matrix_nonempty_predprefix)))) /\ ((cfc_right_matrix_nonempty_predprefixfollowingcode = ((cfc_a_matrix_nonempty_predprefix) + (cfc_b_matrix_nonempty_predprefix)) * S ((cfc_a_matrix_nonempty_predprefix) + (cfc_b_matrix_nonempty_predprefix)) + ((cfc_b_matrix_nonempty_predprefix) + (cfc_b_matrix_nonempty_predprefix))) /\ ((cfc_matrix_matrix_nonempty_predprefixfollowingcode = ((cfc_left_matrix_nonempty_predprefixfollowingcode) + (cfc_right_matrix_nonempty_predprefixfollowingcode)) * S ((cfc_left_matrix_nonempty_predprefixfollowingcode) + (cfc_right_matrix_nonempty_predprefixfollowingcode)) + ((cfc_right_matrix_nonempty_predprefixfollowingcode) + (cfc_right_matrix_nonempty_predprefixfollowingcode))) /\ ((cfc_state_matrix_nonempty_predprefixfollowing) = ((cfc_new_matrix_nonempty_predprefix) + (cfc_matrix_matrix_nonempty_predprefixfollowingcode)) * S ((cfc_new_matrix_nonempty_predprefix) + (cfc_matrix_matrix_nonempty_predprefixfollowingcode)) + ((cfc_matrix_matrix_nonempty_predprefixfollowingcode) + (cfc_matrix_matrix_nonempty_predprefixfollowingcode))))))) /\ (((exists ff_h_matrix_nonempty_predprefixfollowingentry. ff_h_matrix_nonempty_predprefixfollowingentry + S (cfc_state_matrix_nonempty_predprefixfollowing) = S ((S (S cfc_index_matrix_nonempty_predprefix)) * e)) /\ exists ff_q_matrix_nonempty_predprefixfollowingentry. h = ff_q_matrix_nonempty_predprefixfollowingentry * S ((S (S cfc_index_matrix_nonempty_predprefix)) * e) + (cfc_state_matrix_nonempty_predprefixfollowing))))) /\ (cfc_new_matrix_nonempty_predprefix = S ((cfc_quotient_matrix_nonempty_predprefix + cfc_old_matrix_nonempty_predprefix) * S (cfc_quotient_matrix_nonempty_predprefix + cfc_old_matrix_nonempty_predprefix) + (cfc_old_matrix_nonempty_predprefix + cfc_old_matrix_nonempty_predprefix))))))))) /\ ((s = S ((cfc_q_matrix_nonempty_pred + cfc_tail_matrix_nonempty_pred) * S (cfc_q_matrix_nonempty_pred + cfc_tail_matrix_nonempty_pred) + (cfc_tail_matrix_nonempty_pred + cfc_tail_matrix_nonempty_pred))) /\ (((u) = cfc_q_matrix_nonempty_pred * cfc_a_matrix_nonempty_pred + cfc_c_matrix_nonempty_pred) /\ (((U) = cfc_q_matrix_nonempty_pred * cfc_b_matrix_nonempty_pred + cfc_d_matrix_nonempty_pred) /\ (((v) = cfc_a_matrix_nonempty_pred) /\ ((V) = cfc_b_matrix_nonempty_pred))))))
  12. 0012specialize cf_convergent_matrix_successor_elimination (s)
  13. 0013specialize cf_convergent_matrix_successor_elimination (h)
  14. 0014specialize cf_convergent_matrix_successor_elimination (e)
  15. 0015specialize cf_convergent_matrix_successor_elimination (k)
  16. 0016specialize cf_convergent_matrix_successor_elimination (u)
  17. 0017specialize cf_convergent_matrix_successor_elimination (U)
  18. 0018specialize cf_convergent_matrix_successor_elimination (v)
  19. 0019specialize cf_convergent_matrix_successor_elimination (V)
  20. 0020apply cf_convergent_matrix_successor_elimination
  21. 0021exact ht
  22. 0022cases hp
  23. 0023cases hp_witness
  24. 0024cases hp_witness_witness
  25. 0025cases hp_witness_witness_witness
  26. 0026cases hp_witness_witness_witness_witness
  27. 0027cases hp_witness_witness_witness_witness_witness
  28. 0028cases hp_witness_witness_witness_witness_witness_witness
  29. 0029cases hp_witness_witness_witness_witness_witness_witness_right
  30. 0030cases hp_witness_witness_witness_witness_witness_witness_right_right
  31. 0031cases hp_witness_witness_witness_witness_witness_witness_right_right_right
  32. 0032cases hp_witness_witness_witness_witness_witness_witness_right_right_right_right
  33. 0033specialize cell_nonzero (s)
  34. 0034specialize cell_nonzero (x5)
  35. 0035specialize cell_nonzero (x)
  36. 0036apply cell_nonzero
  37. 0037exact hp_witness_witness_witness_witness_witness_witness_right_left
  38. 0038exact hz