BA0033

cf_convergent_matrix_successor_elimination

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

Every nonempty actual prefix computation exposes a tagged first quotient and the exact four matrix recurrence equations.

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_successor. ((exists cfc_state_matrix_successorinitial. ((exists cfc_left_matrix_successorinitialcode cfc_right_matrix_successorinitialcode cfc_matrix_matrix_successorinitialcode. ((cfc_left_matrix_successorinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_matrix_successorinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_matrix_successorinitialcode = ((cfc_left_matrix_successorinitialcode) + (cfc_right_matrix_successorinitialcode)) * S ((cfc_left_matrix_successorinitialcode) + (cfc_right_matrix_successorinitialcode)) + ((cfc_right_matrix_successorinitialcode) + (cfc_right_matrix_successorinitialcode))) /\ ((cfc_state_matrix_successorinitial) = ((cfc_tail_matrix_successor) + (cfc_matrix_matrix_successorinitialcode)) * S ((cfc_tail_matrix_successor) + (cfc_matrix_matrix_successorinitialcode)) + ((cfc_matrix_matrix_successorinitialcode) + (cfc_matrix_matrix_successorinitialcode))))))) /\ (((exists ff_h_matrix_successorinitialentry. ff_h_matrix_successorinitialentry + S (cfc_state_matrix_successorinitial) = S ((S (0)) * e)) /\ exists ff_q_matrix_successorinitialentry. h = ff_q_matrix_successorinitialentry * S ((S (0)) * e) + (cfc_state_matrix_successorinitial))))) /\ ((exists cfc_state_matrix_successorterminal. ((exists cfc_left_matrix_successorterminalcode cfc_right_matrix_successorterminalcode cfc_matrix_matrix_successorterminalcode. ((cfc_left_matrix_successorterminalcode = ((u) + (U)) * S ((u) + (U)) + ((U) + (U))) /\ ((cfc_right_matrix_successorterminalcode = ((v) + (V)) * S ((v) + (V)) + ((V) + (V))) /\ ((cfc_matrix_matrix_successorterminalcode = ((cfc_left_matrix_successorterminalcode) + (cfc_right_matrix_successorterminalcode)) * S ((cfc_left_matrix_successorterminalcode) + (cfc_right_matrix_successorterminalcode)) + ((cfc_right_matrix_successorterminalcode) + (cfc_right_matrix_successorterminalcode))) /\ ((cfc_state_matrix_successorterminal) = ((s) + (cfc_matrix_matrix_successorterminalcode)) * S ((s) + (cfc_matrix_matrix_successorterminalcode)) + ((cfc_matrix_matrix_successorterminalcode) + (cfc_matrix_matrix_successorterminalcode))))))) /\ (((exists ff_h_matrix_successorterminalentry. ff_h_matrix_successorterminalentry + S (cfc_state_matrix_successorterminal) = S ((S (S k)) * e)) /\ exists ff_q_matrix_successorterminalentry. h = ff_q_matrix_successorterminalentry * S ((S (S k)) * e) + (cfc_state_matrix_successorterminal))))) /\ (forall cfc_index_matrix_successor. (exists cfba_gap_matrix_successorbound. cfba_gap_matrix_successorbound + S (cfc_index_matrix_successor) = (S k)) -> exists cfc_old_matrix_successor cfc_a_matrix_successor cfc_b_matrix_successor cfc_c_matrix_successor cfc_d_matrix_successor cfc_new_matrix_successor cfc_quotient_matrix_successor. ((exists cfc_state_matrix_successorprevious. ((exists cfc_left_matrix_successorpreviouscode cfc_right_matrix_successorpreviouscode cfc_matrix_matrix_successorpreviouscode. ((cfc_left_matrix_successorpreviouscode = ((cfc_a_matrix_successor) + (cfc_b_matrix_successor)) * S ((cfc_a_matrix_successor) + (cfc_b_matrix_successor)) + ((cfc_b_matrix_successor) + (cfc_b_matrix_successor))) /\ ((cfc_right_matrix_successorpreviouscode = ((cfc_c_matrix_successor) + (cfc_d_matrix_successor)) * S ((cfc_c_matrix_successor) + (cfc_d_matrix_successor)) + ((cfc_d_matrix_successor) + (cfc_d_matrix_successor))) /\ ((cfc_matrix_matrix_successorpreviouscode = ((cfc_left_matrix_successorpreviouscode) + (cfc_right_matrix_successorpreviouscode)) * S ((cfc_left_matrix_successorpreviouscode) + (cfc_right_matrix_successorpreviouscode)) + ((cfc_right_matrix_successorpreviouscode) + (cfc_right_matrix_successorpreviouscode))) /\ ((cfc_state_matrix_successorprevious) = ((cfc_old_matrix_successor) + (cfc_matrix_matrix_successorpreviouscode)) * S ((cfc_old_matrix_successor) + (cfc_matrix_matrix_successorpreviouscode)) + ((cfc_matrix_matrix_successorpreviouscode) + (cfc_matrix_matrix_successorpreviouscode))))))) /\ (((exists ff_h_matrix_successorpreviousentry. ff_h_matrix_successorpreviousentry + S (cfc_state_matrix_successorprevious) = S ((S (cfc_index_matrix_successor)) * e)) /\ exists ff_q_matrix_successorpreviousentry. h = ff_q_matrix_successorpreviousentry * S ((S (cfc_index_matrix_successor)) * e) + (cfc_state_matrix_successorprevious))))) /\ ((exists cfc_state_matrix_successorfollowing. ((exists cfc_left_matrix_successorfollowingcode cfc_right_matrix_successorfollowingcode cfc_matrix_matrix_successorfollowingcode. ((cfc_left_matrix_successorfollowingcode = (((cfc_quotient_matrix_successor * cfc_a_matrix_successor + cfc_c_matrix_successor)) + ((cfc_quotient_matrix_successor * cfc_b_matrix_successor + cfc_d_matrix_successor))) * S (((cfc_quotient_matrix_successor * cfc_a_matrix_successor + cfc_c_matrix_successor)) + ((cfc_quotient_matrix_successor * cfc_b_matrix_successor + cfc_d_matrix_successor))) + (((cfc_quotient_matrix_successor * cfc_b_matrix_successor + cfc_d_matrix_successor)) + ((cfc_quotient_matrix_successor * cfc_b_matrix_successor + cfc_d_matrix_successor)))) /\ ((cfc_right_matrix_successorfollowingcode = ((cfc_a_matrix_successor) + (cfc_b_matrix_successor)) * S ((cfc_a_matrix_successor) + (cfc_b_matrix_successor)) + ((cfc_b_matrix_successor) + (cfc_b_matrix_successor))) /\ ((cfc_matrix_matrix_successorfollowingcode = ((cfc_left_matrix_successorfollowingcode) + (cfc_right_matrix_successorfollowingcode)) * S ((cfc_left_matrix_successorfollowingcode) + (cfc_right_matrix_successorfollowingcode)) + ((cfc_right_matrix_successorfollowingcode) + (cfc_right_matrix_successorfollowingcode))) /\ ((cfc_state_matrix_successorfollowing) = ((cfc_new_matrix_successor) + (cfc_matrix_matrix_successorfollowingcode)) * S ((cfc_new_matrix_successor) + (cfc_matrix_matrix_successorfollowingcode)) + ((cfc_matrix_matrix_successorfollowingcode) + (cfc_matrix_matrix_successorfollowingcode))))))) /\ (((exists ff_h_matrix_successorfollowingentry. ff_h_matrix_successorfollowingentry + S (cfc_state_matrix_successorfollowing) = S ((S (S cfc_index_matrix_successor)) * e)) /\ exists ff_q_matrix_successorfollowingentry. h = ff_q_matrix_successorfollowingentry * S ((S (S cfc_index_matrix_successor)) * e) + (cfc_state_matrix_successorfollowing))))) /\ (cfc_new_matrix_successor = S ((cfc_quotient_matrix_successor + cfc_old_matrix_successor) * S (cfc_quotient_matrix_successor + cfc_old_matrix_successor) + (cfc_old_matrix_successor + cfc_old_matrix_successor))))))))) -> (exists cfc_tail_matrix_predecessor cfc_a_matrix_predecessor cfc_b_matrix_predecessor cfc_c_matrix_predecessor cfc_d_matrix_predecessor cfc_q_matrix_predecessor. ((exists cfc_tail_matrix_predecessorprefix. ((exists cfc_state_matrix_predecessorprefixinitial. ((exists cfc_left_matrix_predecessorprefixinitialcode cfc_right_matrix_predecessorprefixinitialcode cfc_matrix_matrix_predecessorprefixinitialcode. ((cfc_left_matrix_predecessorprefixinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_matrix_predecessorprefixinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_matrix_predecessorprefixinitialcode = ((cfc_left_matrix_predecessorprefixinitialcode) + (cfc_right_matrix_predecessorprefixinitialcode)) * S ((cfc_left_matrix_predecessorprefixinitialcode) + (cfc_right_matrix_predecessorprefixinitialcode)) + ((cfc_right_matrix_predecessorprefixinitialcode) + (cfc_right_matrix_predecessorprefixinitialcode))) /\ ((cfc_state_matrix_predecessorprefixinitial) = ((cfc_tail_matrix_predecessorprefix) + (cfc_matrix_matrix_predecessorprefixinitialcode)) * S ((cfc_tail_matrix_predecessorprefix) + (cfc_matrix_matrix_predecessorprefixinitialcode)) + ((cfc_matrix_matrix_predecessorprefixinitialcode) + (cfc_matrix_matrix_predecessorprefixinitialcode))))))) /\ (((exists ff_h_matrix_predecessorprefixinitialentry. ff_h_matrix_predecessorprefixinitialentry + S (cfc_state_matrix_predecessorprefixinitial) = S ((S (0)) * e)) /\ exists ff_q_matrix_predecessorprefixinitialentry. h = ff_q_matrix_predecessorprefixinitialentry * S ((S (0)) * e) + (cfc_state_matrix_predecessorprefixinitial))))) /\ ((exists cfc_state_matrix_predecessorprefixterminal. ((exists cfc_left_matrix_predecessorprefixterminalcode cfc_right_matrix_predecessorprefixterminalcode cfc_matrix_matrix_predecessorprefixterminalcode. ((cfc_left_matrix_predecessorprefixterminalcode = ((cfc_a_matrix_predecessor) + (cfc_b_matrix_predecessor)) * S ((cfc_a_matrix_predecessor) + (cfc_b_matrix_predecessor)) + ((cfc_b_matrix_predecessor) + (cfc_b_matrix_predecessor))) /\ ((cfc_right_matrix_predecessorprefixterminalcode = ((cfc_c_matrix_predecessor) + (cfc_d_matrix_predecessor)) * S ((cfc_c_matrix_predecessor) + (cfc_d_matrix_predecessor)) + ((cfc_d_matrix_predecessor) + (cfc_d_matrix_predecessor))) /\ ((cfc_matrix_matrix_predecessorprefixterminalcode = ((cfc_left_matrix_predecessorprefixterminalcode) + (cfc_right_matrix_predecessorprefixterminalcode)) * S ((cfc_left_matrix_predecessorprefixterminalcode) + (cfc_right_matrix_predecessorprefixterminalcode)) + ((cfc_right_matrix_predecessorprefixterminalcode) + (cfc_right_matrix_predecessorprefixterminalcode))) /\ ((cfc_state_matrix_predecessorprefixterminal) = ((cfc_tail_matrix_predecessor) + (cfc_matrix_matrix_predecessorprefixterminalcode)) * S ((cfc_tail_matrix_predecessor) + (cfc_matrix_matrix_predecessorprefixterminalcode)) + ((cfc_matrix_matrix_predecessorprefixterminalcode) + (cfc_matrix_matrix_predecessorprefixterminalcode))))))) /\ (((exists ff_h_matrix_predecessorprefixterminalentry. ff_h_matrix_predecessorprefixterminalentry + S (cfc_state_matrix_predecessorprefixterminal) = S ((S (k)) * e)) /\ exists ff_q_matrix_predecessorprefixterminalentry. h = ff_q_matrix_predecessorprefixterminalentry * S ((S (k)) * e) + (cfc_state_matrix_predecessorprefixterminal))))) /\ (forall cfc_index_matrix_predecessorprefix. (exists cfba_gap_matrix_predecessorprefixbound. cfba_gap_matrix_predecessorprefixbound + S (cfc_index_matrix_predecessorprefix) = (k)) -> exists cfc_old_matrix_predecessorprefix cfc_a_matrix_predecessorprefix cfc_b_matrix_predecessorprefix cfc_c_matrix_predecessorprefix cfc_d_matrix_predecessorprefix cfc_new_matrix_predecessorprefix cfc_quotient_matrix_predecessorprefix. ((exists cfc_state_matrix_predecessorprefixprevious. ((exists cfc_left_matrix_predecessorprefixpreviouscode cfc_right_matrix_predecessorprefixpreviouscode cfc_matrix_matrix_predecessorprefixpreviouscode. ((cfc_left_matrix_predecessorprefixpreviouscode = ((cfc_a_matrix_predecessorprefix) + (cfc_b_matrix_predecessorprefix)) * S ((cfc_a_matrix_predecessorprefix) + (cfc_b_matrix_predecessorprefix)) + ((cfc_b_matrix_predecessorprefix) + (cfc_b_matrix_predecessorprefix))) /\ ((cfc_right_matrix_predecessorprefixpreviouscode = ((cfc_c_matrix_predecessorprefix) + (cfc_d_matrix_predecessorprefix)) * S ((cfc_c_matrix_predecessorprefix) + (cfc_d_matrix_predecessorprefix)) + ((cfc_d_matrix_predecessorprefix) + (cfc_d_matrix_predecessorprefix))) /\ ((cfc_matrix_matrix_predecessorprefixpreviouscode = ((cfc_left_matrix_predecessorprefixpreviouscode) + (cfc_right_matrix_predecessorprefixpreviouscode)) * S ((cfc_left_matrix_predecessorprefixpreviouscode) + (cfc_right_matrix_predecessorprefixpreviouscode)) + ((cfc_right_matrix_predecessorprefixpreviouscode) + (cfc_right_matrix_predecessorprefixpreviouscode))) /\ ((cfc_state_matrix_predecessorprefixprevious) = ((cfc_old_matrix_predecessorprefix) + (cfc_matrix_matrix_predecessorprefixpreviouscode)) * S ((cfc_old_matrix_predecessorprefix) + (cfc_matrix_matrix_predecessorprefixpreviouscode)) + ((cfc_matrix_matrix_predecessorprefixpreviouscode) + (cfc_matrix_matrix_predecessorprefixpreviouscode))))))) /\ (((exists ff_h_matrix_predecessorprefixpreviousentry. ff_h_matrix_predecessorprefixpreviousentry + S (cfc_state_matrix_predecessorprefixprevious) = S ((S (cfc_index_matrix_predecessorprefix)) * e)) /\ exists ff_q_matrix_predecessorprefixpreviousentry. h = ff_q_matrix_predecessorprefixpreviousentry * S ((S (cfc_index_matrix_predecessorprefix)) * e) + (cfc_state_matrix_predecessorprefixprevious))))) /\ ((exists cfc_state_matrix_predecessorprefixfollowing. ((exists cfc_left_matrix_predecessorprefixfollowingcode cfc_right_matrix_predecessorprefixfollowingcode cfc_matrix_matrix_predecessorprefixfollowingcode. ((cfc_left_matrix_predecessorprefixfollowingcode = (((cfc_quotient_matrix_predecessorprefix * cfc_a_matrix_predecessorprefix + cfc_c_matrix_predecessorprefix)) + ((cfc_quotient_matrix_predecessorprefix * cfc_b_matrix_predecessorprefix + cfc_d_matrix_predecessorprefix))) * S (((cfc_quotient_matrix_predecessorprefix * cfc_a_matrix_predecessorprefix + cfc_c_matrix_predecessorprefix)) + ((cfc_quotient_matrix_predecessorprefix * cfc_b_matrix_predecessorprefix + cfc_d_matrix_predecessorprefix))) + (((cfc_quotient_matrix_predecessorprefix * cfc_b_matrix_predecessorprefix + cfc_d_matrix_predecessorprefix)) + ((cfc_quotient_matrix_predecessorprefix * cfc_b_matrix_predecessorprefix + cfc_d_matrix_predecessorprefix)))) /\ ((cfc_right_matrix_predecessorprefixfollowingcode = ((cfc_a_matrix_predecessorprefix) + (cfc_b_matrix_predecessorprefix)) * S ((cfc_a_matrix_predecessorprefix) + (cfc_b_matrix_predecessorprefix)) + ((cfc_b_matrix_predecessorprefix) + (cfc_b_matrix_predecessorprefix))) /\ ((cfc_matrix_matrix_predecessorprefixfollowingcode = ((cfc_left_matrix_predecessorprefixfollowingcode) + (cfc_right_matrix_predecessorprefixfollowingcode)) * S ((cfc_left_matrix_predecessorprefixfollowingcode) + (cfc_right_matrix_predecessorprefixfollowingcode)) + ((cfc_right_matrix_predecessorprefixfollowingcode) + (cfc_right_matrix_predecessorprefixfollowingcode))) /\ ((cfc_state_matrix_predecessorprefixfollowing) = ((cfc_new_matrix_predecessorprefix) + (cfc_matrix_matrix_predecessorprefixfollowingcode)) * S ((cfc_new_matrix_predecessorprefix) + (cfc_matrix_matrix_predecessorprefixfollowingcode)) + ((cfc_matrix_matrix_predecessorprefixfollowingcode) + (cfc_matrix_matrix_predecessorprefixfollowingcode))))))) /\ (((exists ff_h_matrix_predecessorprefixfollowingentry. ff_h_matrix_predecessorprefixfollowingentry + S (cfc_state_matrix_predecessorprefixfollowing) = S ((S (S cfc_index_matrix_predecessorprefix)) * e)) /\ exists ff_q_matrix_predecessorprefixfollowingentry. h = ff_q_matrix_predecessorprefixfollowingentry * S ((S (S cfc_index_matrix_predecessorprefix)) * e) + (cfc_state_matrix_predecessorprefixfollowing))))) /\ (cfc_new_matrix_predecessorprefix = S ((cfc_quotient_matrix_predecessorprefix + cfc_old_matrix_predecessorprefix) * S (cfc_quotient_matrix_predecessorprefix + cfc_old_matrix_predecessorprefix) + (cfc_old_matrix_predecessorprefix + cfc_old_matrix_predecessorprefix))))))))) /\ ((s = S ((cfc_q_matrix_predecessor + cfc_tail_matrix_predecessor) * S (cfc_q_matrix_predecessor + cfc_tail_matrix_predecessor) + (cfc_tail_matrix_predecessor + cfc_tail_matrix_predecessor))) /\ (((u) = cfc_q_matrix_predecessor * cfc_a_matrix_predecessor + cfc_c_matrix_predecessor) /\ (((U) = cfc_q_matrix_predecessor * cfc_b_matrix_predecessor + cfc_d_matrix_predecessor) /\ (((v) = cfc_a_matrix_predecessor) /\ ((V) = cfc_b_matrix_predecessor)))))))

Constructive proof overview

Generated structural guide

Every nonempty actual prefix computation exposes a tagged first quotient and the exact four matrix recurrence equations.

The unchanged tactic script uses 4 declared prerequisites and contains 80 exact native proof lines.

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

Proof neighborhood

Direct dependencies

BA0031 cf_convergent_matrix_state_unique zero_add Stable theorem; checked-use authorized lt_of_lt_of_le Stable theorem; checked-use authorized le_succ_self Stable theorem; checked-use authorized

Direct dependents

BA0034 cf_convergent_matrix_nonempty_list BA003D cf_convergent_euclidean_matrix_step_alignment BA004B cf_convergent_matrix_prefix_functional BA004F cf_convergent_second_column_is_previous_prefix

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

80 script commands · 27 reading checkpoints · 2 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 state unique

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

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
02Separate the logical casesL10–12

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

  1. L10
    cases ht
  2. L11
    cases ht_witness
  3. L12
    cases ht_witness_right
03Establish hsL13–15

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

  1. L13
    have hs · expand full local formula (672 characters)have hs : ∃ cfc_old_matrix_last_step. ∃ cfc_a_matrix_last_step. ∃ cfc_b_matrix_last_step. ∃ cfc_c_matrix_last_step. ∃ cfc_d_matrix_last_step. ∃ cfc_new_matrix_last_step. ∃ cfc_q_matrix_last_step. ConvergentMatrixAt(h,e,k,cfc_old_matrix_last_step,cfc_a_matrix_last_step,cfc_b_matrix_last_step,cfc_c_matrix_last_step,cfc_d_matrix_last_step) ∧ (ConvergentMatrixAt(h,e,S k,cfc_new_matrix_last_step,cfc_q_matrix_last_step · cfc_a_matrix_last_step + cfc_c_matrix_last_step,cfc_q_matrix_last_step · cfc_b_matrix_last_step + cfc_d_matrix_last_step,cfc_a_matrix_last_step,cfc_b_matrix_last_step) ∧ ListCell(cfc_new_matrix_last_step,cfc_q_matrix_last_step,cfc_old_matrix_last_step))
    Definitions: ListCellConvergentMatrixAt
  2. L14
    specialize ht_witness_right_right (k)
  3. L15
    apply ht_witness_right_right
04Construct an explicit witnessL16–16

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

  1. L16
    exists 0
05Use earlier factsL17–17

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

  1. L17
    apply zero_add
06Separate the logical casesL18–26

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

  1. L18
    cases hs
  2. L19
    cases hs_witness
  3. L20
    cases hs_witness_witness
  4. L21
    cases hs_witness_witness_witness
  5. L22
    cases hs_witness_witness_witness_witness
  6. L23
    cases hs_witness_witness_witness_witness_witness
  7. L24
    cases hs_witness_witness_witness_witness_witness_witness
  8. L25
    cases hs_witness_witness_witness_witness_witness_witness_witness
  9. L26
    cases hs_witness_witness_witness_witness_witness_witness_witness_right
07Establish heqL27–36

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

  1. L27
    have heq : ((s = x6) /\ ((u = x7 * x2 + x4) /\ ((U = x7 * x3 + x5) /\ ((v = x2) /\ (V = x3)))))
  2. L28
    specialize cf_convergent_matrix_state_unique (h)
  3. L29
    specialize cf_convergent_matrix_state_unique (e)
  4. L30
    specialize cf_convergent_matrix_state_unique (S k)
  5. L31
    specialize cf_convergent_matrix_state_unique (s)
  6. L32
    specialize cf_convergent_matrix_state_unique (u)
  7. L33
    specialize cf_convergent_matrix_state_unique (U)
  8. L34
    specialize cf_convergent_matrix_state_unique (v)
  9. L35
    specialize cf_convergent_matrix_state_unique (V)
  10. L36
    specialize cf_convergent_matrix_state_unique (x6)
08Use earlier factsL37–43

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

  1. L37
    specialize cf_convergent_matrix_state_unique (x7 * x2 + x4)
  2. L38
    specialize cf_convergent_matrix_state_unique (x7 * x3 + x5)
  3. L39
    specialize cf_convergent_matrix_state_unique (x2)
  4. L40
    specialize cf_convergent_matrix_state_unique (x3)
  5. L41
    apply cf_convergent_matrix_state_unique
  6. L42
    exact ht_witness_right_left
  7. L43
    exact hs_witness_witness_witness_witness_witness_witness_witness_right_left
09Separate the logical casesL44–47

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

  1. L44
    cases heq
  2. L45
    cases heq_right
  3. L46
    cases heq_right_right
  4. L47
    cases heq_right_right_right
10Construct an explicit witnessL48–53

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

  1. L48
    exists x1
  2. L49
    exists x2
  3. L50
    exists x3
  4. L51
    exists x4
  5. L52
    exists x5
  6. L53
    exists x7
11Separate the logical casesL54–54

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

  1. L54
    split
12Construct an explicit witnessL55–55

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

  1. L55
    exists x
13Separate the logical casesL56–56

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

  1. L56
    split
14Use earlier factsL57–57

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

  1. L57
    exact ht_witness_left
15Separate the logical casesL58–58

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

  1. L58
    split
16Use earlier factsL59–59

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

  1. L59
    exact hs_witness_witness_witness_witness_witness_witness_witness_left
17Fix variables and assumptionsL60–61

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

  1. L60
    intro j
  2. L61
    intro hj
18Use earlier factsL62–70

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

  1. L62
    specialize ht_witness_right_right (j)
  2. L63
    apply ht_witness_right_right
  3. L64
    specialize lt_of_lt_of_le (j)
  4. L65
    specialize lt_of_lt_of_le (k)
  5. L66
    specialize lt_of_lt_of_le (S k)
  6. L67
    apply lt_of_lt_of_le
  7. L68
    exact hj
  8. L69
    specialize le_succ_self (k)
  9. L70
    apply le_succ_self
19Separate the logical casesL71–71

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

  1. L71
    split
20Calculate and transport equalitiesL72–72

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

  1. L72
    rewrite heq_left
21Use earlier factsL73–73

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

  1. L73
    exact hs_witness_witness_witness_witness_witness_witness_witness_right_right
22Separate the logical casesL74–74

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

  1. L74
    split
23Use earlier factsL75–75

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

  1. L75
    exact heq_right_left
24Separate the logical casesL76–76

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

  1. L76
    split
25Use earlier factsL77–77

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

  1. L77
    exact heq_right_right_left
26Separate the logical casesL78–78

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

  1. L78
    split
27Use earlier factsL79–80

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

  1. L79
    exact heq_right_right_right_left
  2. L80
    exact heq_right_right_right_right

Library-wide reading audit

Original exact command ledger · 80 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. 0010cases ht
  11. 0011cases ht_witness
  12. 0012cases ht_witness_right
  13. 0013have hs : exists cfc_old_matrix_last_step cfc_a_matrix_last_step cfc_b_matrix_last_step cfc_c_matrix_last_step cfc_d_matrix_last_step cfc_new_matrix_last_step cfc_q_matrix_last_step. ((exists cfc_state_matrix_last_stepprevious. ((exists cfc_left_matrix_last_steppreviouscode cfc_right_matrix_last_steppreviouscode cfc_matrix_matrix_last_steppreviouscode. ((cfc_left_matrix_last_steppreviouscode = ((cfc_a_matrix_last_step) + (cfc_b_matrix_last_step)) * S ((cfc_a_matrix_last_step) + (cfc_b_matrix_last_step)) + ((cfc_b_matrix_last_step) + (cfc_b_matrix_last_step))) /\ ((cfc_right_matrix_last_steppreviouscode = ((cfc_c_matrix_last_step) + (cfc_d_matrix_last_step)) * S ((cfc_c_matrix_last_step) + (cfc_d_matrix_last_step)) + ((cfc_d_matrix_last_step) + (cfc_d_matrix_last_step))) /\ ((cfc_matrix_matrix_last_steppreviouscode = ((cfc_left_matrix_last_steppreviouscode) + (cfc_right_matrix_last_steppreviouscode)) * S ((cfc_left_matrix_last_steppreviouscode) + (cfc_right_matrix_last_steppreviouscode)) + ((cfc_right_matrix_last_steppreviouscode) + (cfc_right_matrix_last_steppreviouscode))) /\ ((cfc_state_matrix_last_stepprevious) = ((cfc_old_matrix_last_step) + (cfc_matrix_matrix_last_steppreviouscode)) * S ((cfc_old_matrix_last_step) + (cfc_matrix_matrix_last_steppreviouscode)) + ((cfc_matrix_matrix_last_steppreviouscode) + (cfc_matrix_matrix_last_steppreviouscode))))))) /\ (((exists ff_h_matrix_last_steppreviousentry. ff_h_matrix_last_steppreviousentry + S (cfc_state_matrix_last_stepprevious) = S ((S (k)) * e)) /\ exists ff_q_matrix_last_steppreviousentry. h = ff_q_matrix_last_steppreviousentry * S ((S (k)) * e) + (cfc_state_matrix_last_stepprevious))))) /\ ((exists cfc_state_matrix_last_stepfollowing. ((exists cfc_left_matrix_last_stepfollowingcode cfc_right_matrix_last_stepfollowingcode cfc_matrix_matrix_last_stepfollowingcode. ((cfc_left_matrix_last_stepfollowingcode = (((cfc_q_matrix_last_step * cfc_a_matrix_last_step + cfc_c_matrix_last_step)) + ((cfc_q_matrix_last_step * cfc_b_matrix_last_step + cfc_d_matrix_last_step))) * S (((cfc_q_matrix_last_step * cfc_a_matrix_last_step + cfc_c_matrix_last_step)) + ((cfc_q_matrix_last_step * cfc_b_matrix_last_step + cfc_d_matrix_last_step))) + (((cfc_q_matrix_last_step * cfc_b_matrix_last_step + cfc_d_matrix_last_step)) + ((cfc_q_matrix_last_step * cfc_b_matrix_last_step + cfc_d_matrix_last_step)))) /\ ((cfc_right_matrix_last_stepfollowingcode = ((cfc_a_matrix_last_step) + (cfc_b_matrix_last_step)) * S ((cfc_a_matrix_last_step) + (cfc_b_matrix_last_step)) + ((cfc_b_matrix_last_step) + (cfc_b_matrix_last_step))) /\ ((cfc_matrix_matrix_last_stepfollowingcode = ((cfc_left_matrix_last_stepfollowingcode) + (cfc_right_matrix_last_stepfollowingcode)) * S ((cfc_left_matrix_last_stepfollowingcode) + (cfc_right_matrix_last_stepfollowingcode)) + ((cfc_right_matrix_last_stepfollowingcode) + (cfc_right_matrix_last_stepfollowingcode))) /\ ((cfc_state_matrix_last_stepfollowing) = ((cfc_new_matrix_last_step) + (cfc_matrix_matrix_last_stepfollowingcode)) * S ((cfc_new_matrix_last_step) + (cfc_matrix_matrix_last_stepfollowingcode)) + ((cfc_matrix_matrix_last_stepfollowingcode) + (cfc_matrix_matrix_last_stepfollowingcode))))))) /\ (((exists ff_h_matrix_last_stepfollowingentry. ff_h_matrix_last_stepfollowingentry + S (cfc_state_matrix_last_stepfollowing) = S ((S (S (k))) * e)) /\ exists ff_q_matrix_last_stepfollowingentry. h = ff_q_matrix_last_stepfollowingentry * S ((S (S (k))) * e) + (cfc_state_matrix_last_stepfollowing))))) /\ (cfc_new_matrix_last_step = S ((cfc_q_matrix_last_step + cfc_old_matrix_last_step) * S (cfc_q_matrix_last_step + cfc_old_matrix_last_step) + (cfc_old_matrix_last_step + cfc_old_matrix_last_step)))))
  14. 0014specialize ht_witness_right_right (k)
  15. 0015apply ht_witness_right_right
  16. 0016exists 0
  17. 0017apply zero_add
  18. 0018cases hs
  19. 0019cases hs_witness
  20. 0020cases hs_witness_witness
  21. 0021cases hs_witness_witness_witness
  22. 0022cases hs_witness_witness_witness_witness
  23. 0023cases hs_witness_witness_witness_witness_witness
  24. 0024cases hs_witness_witness_witness_witness_witness_witness
  25. 0025cases hs_witness_witness_witness_witness_witness_witness_witness
  26. 0026cases hs_witness_witness_witness_witness_witness_witness_witness_right
  27. 0027have heq : ((s = x6) /\ ((u = x7 * x2 + x4) /\ ((U = x7 * x3 + x5) /\ ((v = x2) /\ (V = x3)))))
  28. 0028specialize cf_convergent_matrix_state_unique (h)
  29. 0029specialize cf_convergent_matrix_state_unique (e)
  30. 0030specialize cf_convergent_matrix_state_unique (S k)
  31. 0031specialize cf_convergent_matrix_state_unique (s)
  32. 0032specialize cf_convergent_matrix_state_unique (u)
  33. 0033specialize cf_convergent_matrix_state_unique (U)
  34. 0034specialize cf_convergent_matrix_state_unique (v)
  35. 0035specialize cf_convergent_matrix_state_unique (V)
  36. 0036specialize cf_convergent_matrix_state_unique (x6)
  37. 0037specialize cf_convergent_matrix_state_unique (x7 * x2 + x4)
  38. 0038specialize cf_convergent_matrix_state_unique (x7 * x3 + x5)
  39. 0039specialize cf_convergent_matrix_state_unique (x2)
  40. 0040specialize cf_convergent_matrix_state_unique (x3)
  41. 0041apply cf_convergent_matrix_state_unique
  42. 0042exact ht_witness_right_left
  43. 0043exact hs_witness_witness_witness_witness_witness_witness_witness_right_left
  44. 0044cases heq
  45. 0045cases heq_right
  46. 0046cases heq_right_right
  47. 0047cases heq_right_right_right
  48. 0048exists x1
  49. 0049exists x2
  50. 0050exists x3
  51. 0051exists x4
  52. 0052exists x5
  53. 0053exists x7
  54. 0054split
  55. 0055exists x
  56. 0056split
  57. 0057exact ht_witness_left
  58. 0058split
  59. 0059exact hs_witness_witness_witness_witness_witness_witness_witness_left
  60. 0060intro j
  61. 0061intro hj
  62. 0062specialize ht_witness_right_right (j)
  63. 0063apply ht_witness_right_right
  64. 0064specialize lt_of_lt_of_le (j)
  65. 0065specialize lt_of_lt_of_le (k)
  66. 0066specialize lt_of_lt_of_le (S k)
  67. 0067apply lt_of_lt_of_le
  68. 0068exact hj
  69. 0069specialize le_succ_self (k)
  70. 0070apply le_succ_self
  71. 0071split
  72. 0072rewrite heq_left
  73. 0073exact hs_witness_witness_witness_witness_witness_witness_witness_right_right
  74. 0074split
  75. 0075exact heq_right_left
  76. 0076split
  77. 0077exact heq_right_right_left
  78. 0078split
  79. 0079exact heq_right_right_right_left
  80. 0080exact heq_right_right_right_right