BA004B

cf_convergent_matrix_prefix_functional

HA induction proves the genuine quotient-prefix matrix is independent of its beta certificate and has unique actual entries for every tagged list and index.

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. ∀ H. ∀ E. ∀ u. ∀ U. ∀ v. ∀ V. ∀ a. ∀ A. ∀ b. ∀ B. ConvergentMatrixTrace(s,h,e,k,u,U,v,V) → ConvergentMatrixTrace(s,H,E,k,a,A,b,B) → u = a ∧ (U = A ∧ (v = b ∧ V = B))

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) · 4

Actual proof prerequisites

cf_convergent_matrix_empty_eliminationcf_convergent_matrix_successor_eliminationcell_functional · checked external prerequisitecf_convergent_matrix_list_transport
Original expanded first-order statement 
forall k s h e H E u U v V a A b B. (exists cfc_tail_functional_first. ((exists cfc_state_functional_firstinitial. ((exists cfc_left_functional_firstinitialcode cfc_right_functional_firstinitialcode cfc_matrix_functional_firstinitialcode. ((cfc_left_functional_firstinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_functional_firstinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_functional_firstinitialcode = ((cfc_left_functional_firstinitialcode) + (cfc_right_functional_firstinitialcode)) * S ((cfc_left_functional_firstinitialcode) + (cfc_right_functional_firstinitialcode)) + ((cfc_right_functional_firstinitialcode) + (cfc_right_functional_firstinitialcode))) /\ ((cfc_state_functional_firstinitial) = ((cfc_tail_functional_first) + (cfc_matrix_functional_firstinitialcode)) * S ((cfc_tail_functional_first) + (cfc_matrix_functional_firstinitialcode)) + ((cfc_matrix_functional_firstinitialcode) + (cfc_matrix_functional_firstinitialcode))))))) /\ (((exists ff_h_functional_firstinitialentry. ff_h_functional_firstinitialentry + S (cfc_state_functional_firstinitial) = S ((S (0)) * e)) /\ exists ff_q_functional_firstinitialentry. h = ff_q_functional_firstinitialentry * S ((S (0)) * e) + (cfc_state_functional_firstinitial))))) /\ ((exists cfc_state_functional_firstterminal. ((exists cfc_left_functional_firstterminalcode cfc_right_functional_firstterminalcode cfc_matrix_functional_firstterminalcode. ((cfc_left_functional_firstterminalcode = ((u) + (U)) * S ((u) + (U)) + ((U) + (U))) /\ ((cfc_right_functional_firstterminalcode = ((v) + (V)) * S ((v) + (V)) + ((V) + (V))) /\ ((cfc_matrix_functional_firstterminalcode = ((cfc_left_functional_firstterminalcode) + (cfc_right_functional_firstterminalcode)) * S ((cfc_left_functional_firstterminalcode) + (cfc_right_functional_firstterminalcode)) + ((cfc_right_functional_firstterminalcode) + (cfc_right_functional_firstterminalcode))) /\ ((cfc_state_functional_firstterminal) = ((s) + (cfc_matrix_functional_firstterminalcode)) * S ((s) + (cfc_matrix_functional_firstterminalcode)) + ((cfc_matrix_functional_firstterminalcode) + (cfc_matrix_functional_firstterminalcode))))))) /\ (((exists ff_h_functional_firstterminalentry. ff_h_functional_firstterminalentry + S (cfc_state_functional_firstterminal) = S ((S (k)) * e)) /\ exists ff_q_functional_firstterminalentry. h = ff_q_functional_firstterminalentry * S ((S (k)) * e) + (cfc_state_functional_firstterminal))))) /\ (forall cfc_index_functional_first. (exists cfba_gap_functional_firstbound. cfba_gap_functional_firstbound + S (cfc_index_functional_first) = (k)) -> exists cfc_old_functional_first cfc_a_functional_first cfc_b_functional_first cfc_c_functional_first cfc_d_functional_first cfc_new_functional_first cfc_quotient_functional_first. ((exists cfc_state_functional_firstprevious. ((exists cfc_left_functional_firstpreviouscode cfc_right_functional_firstpreviouscode cfc_matrix_functional_firstpreviouscode. ((cfc_left_functional_firstpreviouscode = ((cfc_a_functional_first) + (cfc_b_functional_first)) * S ((cfc_a_functional_first) + (cfc_b_functional_first)) + ((cfc_b_functional_first) + (cfc_b_functional_first))) /\ ((cfc_right_functional_firstpreviouscode = ((cfc_c_functional_first) + (cfc_d_functional_first)) * S ((cfc_c_functional_first) + (cfc_d_functional_first)) + ((cfc_d_functional_first) + (cfc_d_functional_first))) /\ ((cfc_matrix_functional_firstpreviouscode = ((cfc_left_functional_firstpreviouscode) + (cfc_right_functional_firstpreviouscode)) * S ((cfc_left_functional_firstpreviouscode) + (cfc_right_functional_firstpreviouscode)) + ((cfc_right_functional_firstpreviouscode) + (cfc_right_functional_firstpreviouscode))) /\ ((cfc_state_functional_firstprevious) = ((cfc_old_functional_first) + (cfc_matrix_functional_firstpreviouscode)) * S ((cfc_old_functional_first) + (cfc_matrix_functional_firstpreviouscode)) + ((cfc_matrix_functional_firstpreviouscode) + (cfc_matrix_functional_firstpreviouscode))))))) /\ (((exists ff_h_functional_firstpreviousentry. ff_h_functional_firstpreviousentry + S (cfc_state_functional_firstprevious) = S ((S (cfc_index_functional_first)) * e)) /\ exists ff_q_functional_firstpreviousentry. h = ff_q_functional_firstpreviousentry * S ((S (cfc_index_functional_first)) * e) + (cfc_state_functional_firstprevious))))) /\ ((exists cfc_state_functional_firstfollowing. ((exists cfc_left_functional_firstfollowingcode cfc_right_functional_firstfollowingcode cfc_matrix_functional_firstfollowingcode. ((cfc_left_functional_firstfollowingcode = (((cfc_quotient_functional_first * cfc_a_functional_first + cfc_c_functional_first)) + ((cfc_quotient_functional_first * cfc_b_functional_first + cfc_d_functional_first))) * S (((cfc_quotient_functional_first * cfc_a_functional_first + cfc_c_functional_first)) + ((cfc_quotient_functional_first * cfc_b_functional_first + cfc_d_functional_first))) + (((cfc_quotient_functional_first * cfc_b_functional_first + cfc_d_functional_first)) + ((cfc_quotient_functional_first * cfc_b_functional_first + cfc_d_functional_first)))) /\ ((cfc_right_functional_firstfollowingcode = ((cfc_a_functional_first) + (cfc_b_functional_first)) * S ((cfc_a_functional_first) + (cfc_b_functional_first)) + ((cfc_b_functional_first) + (cfc_b_functional_first))) /\ ((cfc_matrix_functional_firstfollowingcode = ((cfc_left_functional_firstfollowingcode) + (cfc_right_functional_firstfollowingcode)) * S ((cfc_left_functional_firstfollowingcode) + (cfc_right_functional_firstfollowingcode)) + ((cfc_right_functional_firstfollowingcode) + (cfc_right_functional_firstfollowingcode))) /\ ((cfc_state_functional_firstfollowing) = ((cfc_new_functional_first) + (cfc_matrix_functional_firstfollowingcode)) * S ((cfc_new_functional_first) + (cfc_matrix_functional_firstfollowingcode)) + ((cfc_matrix_functional_firstfollowingcode) + (cfc_matrix_functional_firstfollowingcode))))))) /\ (((exists ff_h_functional_firstfollowingentry. ff_h_functional_firstfollowingentry + S (cfc_state_functional_firstfollowing) = S ((S (S cfc_index_functional_first)) * e)) /\ exists ff_q_functional_firstfollowingentry. h = ff_q_functional_firstfollowingentry * S ((S (S cfc_index_functional_first)) * e) + (cfc_state_functional_firstfollowing))))) /\ (cfc_new_functional_first = S ((cfc_quotient_functional_first + cfc_old_functional_first) * S (cfc_quotient_functional_first + cfc_old_functional_first) + (cfc_old_functional_first + cfc_old_functional_first))))))))) -> (exists cfc_tail_functional_second. ((exists cfc_state_functional_secondinitial. ((exists cfc_left_functional_secondinitialcode cfc_right_functional_secondinitialcode cfc_matrix_functional_secondinitialcode. ((cfc_left_functional_secondinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_functional_secondinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_functional_secondinitialcode = ((cfc_left_functional_secondinitialcode) + (cfc_right_functional_secondinitialcode)) * S ((cfc_left_functional_secondinitialcode) + (cfc_right_functional_secondinitialcode)) + ((cfc_right_functional_secondinitialcode) + (cfc_right_functional_secondinitialcode))) /\ ((cfc_state_functional_secondinitial) = ((cfc_tail_functional_second) + (cfc_matrix_functional_secondinitialcode)) * S ((cfc_tail_functional_second) + (cfc_matrix_functional_secondinitialcode)) + ((cfc_matrix_functional_secondinitialcode) + (cfc_matrix_functional_secondinitialcode))))))) /\ (((exists ff_h_functional_secondinitialentry. ff_h_functional_secondinitialentry + S (cfc_state_functional_secondinitial) = S ((S (0)) * E)) /\ exists ff_q_functional_secondinitialentry. H = ff_q_functional_secondinitialentry * S ((S (0)) * E) + (cfc_state_functional_secondinitial))))) /\ ((exists cfc_state_functional_secondterminal. ((exists cfc_left_functional_secondterminalcode cfc_right_functional_secondterminalcode cfc_matrix_functional_secondterminalcode. ((cfc_left_functional_secondterminalcode = ((a) + (A)) * S ((a) + (A)) + ((A) + (A))) /\ ((cfc_right_functional_secondterminalcode = ((b) + (B)) * S ((b) + (B)) + ((B) + (B))) /\ ((cfc_matrix_functional_secondterminalcode = ((cfc_left_functional_secondterminalcode) + (cfc_right_functional_secondterminalcode)) * S ((cfc_left_functional_secondterminalcode) + (cfc_right_functional_secondterminalcode)) + ((cfc_right_functional_secondterminalcode) + (cfc_right_functional_secondterminalcode))) /\ ((cfc_state_functional_secondterminal) = ((s) + (cfc_matrix_functional_secondterminalcode)) * S ((s) + (cfc_matrix_functional_secondterminalcode)) + ((cfc_matrix_functional_secondterminalcode) + (cfc_matrix_functional_secondterminalcode))))))) /\ (((exists ff_h_functional_secondterminalentry. ff_h_functional_secondterminalentry + S (cfc_state_functional_secondterminal) = S ((S (k)) * E)) /\ exists ff_q_functional_secondterminalentry. H = ff_q_functional_secondterminalentry * S ((S (k)) * E) + (cfc_state_functional_secondterminal))))) /\ (forall cfc_index_functional_second. (exists cfba_gap_functional_secondbound. cfba_gap_functional_secondbound + S (cfc_index_functional_second) = (k)) -> exists cfc_old_functional_second cfc_a_functional_second cfc_b_functional_second cfc_c_functional_second cfc_d_functional_second cfc_new_functional_second cfc_quotient_functional_second. ((exists cfc_state_functional_secondprevious. ((exists cfc_left_functional_secondpreviouscode cfc_right_functional_secondpreviouscode cfc_matrix_functional_secondpreviouscode. ((cfc_left_functional_secondpreviouscode = ((cfc_a_functional_second) + (cfc_b_functional_second)) * S ((cfc_a_functional_second) + (cfc_b_functional_second)) + ((cfc_b_functional_second) + (cfc_b_functional_second))) /\ ((cfc_right_functional_secondpreviouscode = ((cfc_c_functional_second) + (cfc_d_functional_second)) * S ((cfc_c_functional_second) + (cfc_d_functional_second)) + ((cfc_d_functional_second) + (cfc_d_functional_second))) /\ ((cfc_matrix_functional_secondpreviouscode = ((cfc_left_functional_secondpreviouscode) + (cfc_right_functional_secondpreviouscode)) * S ((cfc_left_functional_secondpreviouscode) + (cfc_right_functional_secondpreviouscode)) + ((cfc_right_functional_secondpreviouscode) + (cfc_right_functional_secondpreviouscode))) /\ ((cfc_state_functional_secondprevious) = ((cfc_old_functional_second) + (cfc_matrix_functional_secondpreviouscode)) * S ((cfc_old_functional_second) + (cfc_matrix_functional_secondpreviouscode)) + ((cfc_matrix_functional_secondpreviouscode) + (cfc_matrix_functional_secondpreviouscode))))))) /\ (((exists ff_h_functional_secondpreviousentry. ff_h_functional_secondpreviousentry + S (cfc_state_functional_secondprevious) = S ((S (cfc_index_functional_second)) * E)) /\ exists ff_q_functional_secondpreviousentry. H = ff_q_functional_secondpreviousentry * S ((S (cfc_index_functional_second)) * E) + (cfc_state_functional_secondprevious))))) /\ ((exists cfc_state_functional_secondfollowing. ((exists cfc_left_functional_secondfollowingcode cfc_right_functional_secondfollowingcode cfc_matrix_functional_secondfollowingcode. ((cfc_left_functional_secondfollowingcode = (((cfc_quotient_functional_second * cfc_a_functional_second + cfc_c_functional_second)) + ((cfc_quotient_functional_second * cfc_b_functional_second + cfc_d_functional_second))) * S (((cfc_quotient_functional_second * cfc_a_functional_second + cfc_c_functional_second)) + ((cfc_quotient_functional_second * cfc_b_functional_second + cfc_d_functional_second))) + (((cfc_quotient_functional_second * cfc_b_functional_second + cfc_d_functional_second)) + ((cfc_quotient_functional_second * cfc_b_functional_second + cfc_d_functional_second)))) /\ ((cfc_right_functional_secondfollowingcode = ((cfc_a_functional_second) + (cfc_b_functional_second)) * S ((cfc_a_functional_second) + (cfc_b_functional_second)) + ((cfc_b_functional_second) + (cfc_b_functional_second))) /\ ((cfc_matrix_functional_secondfollowingcode = ((cfc_left_functional_secondfollowingcode) + (cfc_right_functional_secondfollowingcode)) * S ((cfc_left_functional_secondfollowingcode) + (cfc_right_functional_secondfollowingcode)) + ((cfc_right_functional_secondfollowingcode) + (cfc_right_functional_secondfollowingcode))) /\ ((cfc_state_functional_secondfollowing) = ((cfc_new_functional_second) + (cfc_matrix_functional_secondfollowingcode)) * S ((cfc_new_functional_second) + (cfc_matrix_functional_secondfollowingcode)) + ((cfc_matrix_functional_secondfollowingcode) + (cfc_matrix_functional_secondfollowingcode))))))) /\ (((exists ff_h_functional_secondfollowingentry. ff_h_functional_secondfollowingentry + S (cfc_state_functional_secondfollowing) = S ((S (S cfc_index_functional_second)) * E)) /\ exists ff_q_functional_secondfollowingentry. H = ff_q_functional_secondfollowingentry * S ((S (S cfc_index_functional_second)) * E) + (cfc_state_functional_secondfollowing))))) /\ (cfc_new_functional_second = S ((cfc_quotient_functional_second + cfc_old_functional_second) * S (cfc_quotient_functional_second + cfc_old_functional_second) + (cfc_old_functional_second + cfc_old_functional_second))))))))) -> ((u = a) /\ ((U = A) /\ ((v = b) /\ (V = B))))

Complete tactic proof in conservative notation

All 195 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

195 script commands · 62 reading checkpoints · 6 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 (3)
cf convergent matrix empty eliminationcf convergent matrix successor eliminationcf convergent matrix list transport
01Induction on kL1–10

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 H
  6. L6
    intro E
  7. L7
    intro u
  8. L8
    intro U
  9. L9
    intro v
  10. L10
    intro V
02Fix variables and assumptionsL11–16

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

  1. L11
    intro a
  2. L12
    intro A
  3. L13
    intro b
  4. L14
    intro B
  5. L15
    intro hfirst
  6. L16
    intro hsecond
03Establish hleftL17–26

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

  1. L17
    have hleft : ((u = 1) /\ ((U = 0) /\ ((v = 0) /\ (V = 1))))
  2. L18
    specialize cf_convergent_matrix_empty_elimination (s)
  3. L19
    specialize cf_convergent_matrix_empty_elimination (h)
  4. L20
    specialize cf_convergent_matrix_empty_elimination (e)
  5. L21
    specialize cf_convergent_matrix_empty_elimination (u)
  6. L22
    specialize cf_convergent_matrix_empty_elimination (U)
  7. L23
    specialize cf_convergent_matrix_empty_elimination (v)
  8. L24
    specialize cf_convergent_matrix_empty_elimination (V)
  9. L25
    apply cf_convergent_matrix_empty_elimination
  10. L26
    exact hfirst
04Establish hrightL27–36

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

  1. L27
    have hright : ((a = 1) /\ ((A = 0) /\ ((b = 0) /\ (B = 1))))
  2. L28
    specialize cf_convergent_matrix_empty_elimination (s)
  3. L29
    specialize cf_convergent_matrix_empty_elimination (H)
  4. L30
    specialize cf_convergent_matrix_empty_elimination (E)
  5. L31
    specialize cf_convergent_matrix_empty_elimination (a)
  6. L32
    specialize cf_convergent_matrix_empty_elimination (A)
  7. L33
    specialize cf_convergent_matrix_empty_elimination (b)
  8. L34
    specialize cf_convergent_matrix_empty_elimination (B)
  9. L35
    apply cf_convergent_matrix_empty_elimination
  10. L36
    exact hsecond
05Separate the logical casesL37–43

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

  1. L37
    cases hleft
  2. L38
    cases hleft_right
  3. L39
    cases hleft_right_right
  4. L40
    cases hright
  5. L41
    cases hright_right
  6. L42
    cases hright_right_right
  7. L43
    split
06Calculate and transport equalitiesL44–44

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

  1. L44
    trans 1
07Use earlier factsL45–45

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

  1. L45
    exact hleft_left
08Calculate and transport equalitiesL46–46

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

  1. L46
    symm
09Use earlier factsL47–47

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

  1. L47
    exact hright_left
10Separate the logical casesL48–48

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

  1. L48
    split
11Calculate and transport equalitiesL49–49

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

  1. L49
    trans 0
12Use earlier factsL50–50

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

  1. L50
    exact hleft_right_left
13Calculate and transport equalitiesL51–51

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

  1. L51
    symm
14Use earlier factsL52–52

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

  1. L52
    exact hright_right_left
15Separate the logical casesL53–53

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

  1. L53
    split
16Calculate and transport equalitiesL54–54

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

  1. L54
    trans 0
17Use earlier factsL55–55

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

  1. L55
    exact hleft_right_right_left
18Calculate and transport equalitiesL56–56

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

  1. L56
    symm
19Use earlier factsL57–57

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

  1. L57
    exact hright_right_right_left
20Calculate and transport equalitiesL58–58

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

  1. L58
    trans 1
21Use earlier factsL59–59

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

  1. L59
    exact hleft_right_right_right
22Calculate and transport equalitiesL60–60

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

  1. L60
    symm
23Use earlier factsL61–61

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

  1. L61
    exact hright_right_right_right
24Fix variables and assumptionsL62–71

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

  1. L62
    intro s
  2. L63
    intro h
  3. L64
    intro e
  4. L65
    intro H
  5. L66
    intro E
  6. L67
    intro u
  7. L68
    intro U
  8. L69
    intro v
  9. L70
    intro V
  10. L71
    intro a
25Fix variables and assumptionsL72–76

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

  1. L72
    intro A
  2. L73
    intro b
  3. L74
    intro B
  4. L75
    intro hfirst
  5. L76
    intro hsecond
26Establish hleftL77–86

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

  1. L77
    have hleft : ∃ cfc_tail_functional_left. ∃ cfc_a_functional_left. ∃ cfc_b_functional_left. ∃ cfc_c_functional_left. ∃ cfc_d_functional_left. ∃ cfc_q_functional_left. ConvergentMatrixTrace(cfc_tail_functional_left,h,e,k,cfc_a_functional_left,cfc_b_functional_left,cfc_c_functional_left,cfc_d_functional_left) ∧ (ListCell(s,cfc_q_functional_left,cfc_tail_functional_left) ∧ (u = cfc_q_functional_left · cfc_a_functional_left + cfc_c_functional_left ∧ (U = cfc_q_functional_left · cfc_b_functional_left + cfc_d_functional_left ∧ (v = cfc_a_functional_left ∧ V = cfc_b_functional_left))))Definitions: ConvergentMatrixTrace(cfc_tail_functional_left,h,e,k,cfc_a_functional_left,cfc_b_functional_left,cfc_c_functional_left,cfc_d_functional_left)ListCell(s,cfc_q_functional_left,cfc_tail_functional_left)Original native command in the exact edition
  2. L78
    specialize cf_convergent_matrix_successor_elimination (s)
  3. L79
    specialize cf_convergent_matrix_successor_elimination (h)
  4. L80
    specialize cf_convergent_matrix_successor_elimination (e)
  5. L81
    specialize cf_convergent_matrix_successor_elimination (k)
  6. L82
    specialize cf_convergent_matrix_successor_elimination (u)
  7. L83
    specialize cf_convergent_matrix_successor_elimination (U)
  8. L84
    specialize cf_convergent_matrix_successor_elimination (v)
  9. L85
    specialize cf_convergent_matrix_successor_elimination (V)
  10. L86
    apply cf_convergent_matrix_successor_elimination
27Use earlier factsL87–87

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

  1. L87
    exact hfirst
28Establish hrightL88–97

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

  1. L88
    have hright · expand full local formula (606 characters)have hright : ∃ cfc_tail_functional_right. ∃ cfc_a_functional_right. ∃ cfc_b_functional_right. ∃ cfc_c_functional_right. ∃ cfc_d_functional_right. ∃ cfc_q_functional_right. ConvergentMatrixTrace(cfc_tail_functional_right,H,E,k,cfc_a_functional_right,cfc_b_functional_right,cfc_c_functional_right,cfc_d_functional_right) ∧ (ListCell(s,cfc_q_functional_right,cfc_tail_functional_right) ∧ (a = cfc_q_functional_right · cfc_a_functional_right + cfc_c_functional_right ∧ (A = cfc_q_functional_right · cfc_b_functional_right + cfc_d_functional_right ∧ (b = cfc_a_functional_right ∧ B = cfc_b_functional_right))))
    Definitions: ConvergentMatrixTrace(cfc_tail_functional_right,H,E,k,cfc_a_functional_right,cfc_b_functional_right,cfc_c_functional_right,cfc_d_functional_right)ListCell(s,cfc_q_functional_right,cfc_tail_functional_right)Original native command in the exact edition
  2. L89
    specialize cf_convergent_matrix_successor_elimination (s)
  3. L90
    specialize cf_convergent_matrix_successor_elimination (H)
  4. L91
    specialize cf_convergent_matrix_successor_elimination (E)
  5. L92
    specialize cf_convergent_matrix_successor_elimination (k)
  6. L93
    specialize cf_convergent_matrix_successor_elimination (a)
  7. L94
    specialize cf_convergent_matrix_successor_elimination (A)
  8. L95
    specialize cf_convergent_matrix_successor_elimination (b)
  9. L96
    specialize cf_convergent_matrix_successor_elimination (B)
  10. L97
    apply cf_convergent_matrix_successor_elimination
29Use earlier factsL98–98

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

  1. L98
    exact hsecond
30Separate the logical casesL99–108

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

  1. L99
    cases hleft
  2. L100
    cases hleft_witness
  3. L101
    cases hleft_witness_witness
  4. L102
    cases hleft_witness_witness_witness
  5. L103
    cases hleft_witness_witness_witness_witness
  6. L104
    cases hleft_witness_witness_witness_witness_witness
  7. L105
    cases hright
  8. L106
    cases hright_witness
  9. L107
    cases hright_witness_witness
  10. L108
    cases hright_witness_witness_witness
31Separate the logical casesL109–118

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

  1. L109
    cases hright_witness_witness_witness_witness
  2. L110
    cases hright_witness_witness_witness_witness_witness
  3. L111
    cases hleft_witness_witness_witness_witness_witness_witness
  4. L112
    cases hleft_witness_witness_witness_witness_witness_witness_right
  5. L113
    cases hleft_witness_witness_witness_witness_witness_witness_right_right
  6. L114
    cases hleft_witness_witness_witness_witness_witness_witness_right_right_right
  7. L115
    cases hleft_witness_witness_witness_witness_witness_witness_right_right_right_right
  8. L116
    cases hright_witness_witness_witness_witness_witness_witness
  9. L117
    cases hright_witness_witness_witness_witness_witness_witness_right
  10. L118
    cases hright_witness_witness_witness_witness_witness_witness_right_right
32Separate the logical casesL119–120

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

  1. L119
    cases hright_witness_witness_witness_witness_witness_witness_right_right_right
  2. L120
    cases hright_witness_witness_witness_witness_witness_witness_right_right_right_right
33Establish hcellL121–129

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

  1. L121
    have hcell : x5 = x11 /\ x = x6
  2. L122
    specialize cell_functional (s)
  3. L123
    specialize cell_functional (x5)
  4. L124
    specialize cell_functional (x)
  5. L125
    specialize cell_functional (x11)
  6. L126
    specialize cell_functional (x6)
  7. L127
    apply cell_functional
  8. L128
    exact hleft_witness_witness_witness_witness_witness_witness_right_left
  9. L129
    exact hright_witness_witness_witness_witness_witness_witness_right_left
34Separate the logical casesL130–130

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

  1. L130
    cases hcell
35Establish hinnerL131–140

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

  1. L131
    have hinner : ((x1 = x7) /\ ((x2 = x8) /\ ((x3 = x9) /\ (x4 = x10))))
  2. L132
    specialize IH (x)
  3. L133
    specialize IH (h)
  4. L134
    specialize IH (e)
  5. L135
    specialize IH (H)
  6. L136
    specialize IH (E)
  7. L137
    specialize IH (x1)
  8. L138
    specialize IH (x2)
  9. L139
    specialize IH (x3)
  10. L140
    specialize IH (x4)
36Use earlier factsL141–150

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

  1. L141
    specialize IH (x7)
  2. L142
    specialize IH (x8)
  3. L143
    specialize IH (x9)
  4. L144
    specialize IH (x10)
  5. L145
    apply IH
  6. L146
    exact hleft_witness_witness_witness_witness_witness_witness_left
  7. L147
    specialize cf_convergent_matrix_list_transport (x6)
  8. L148
    specialize cf_convergent_matrix_list_transport (x)
  9. L149
    specialize cf_convergent_matrix_list_transport (H)
  10. L150
    specialize cf_convergent_matrix_list_transport (E)
37Use earlier factsL151–156

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

  1. L151
    specialize cf_convergent_matrix_list_transport (k)
  2. L152
    specialize cf_convergent_matrix_list_transport (x7)
  3. L153
    specialize cf_convergent_matrix_list_transport (x8)
  4. L154
    specialize cf_convergent_matrix_list_transport (x9)
  5. L155
    specialize cf_convergent_matrix_list_transport (x10)
  6. L156
    apply cf_convergent_matrix_list_transport
38Calculate and transport equalitiesL157–157

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

  1. L157
    symm
39Use earlier factsL158–159

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

  1. L158
    exact hcell_right
  2. L159
    exact hright_witness_witness_witness_witness_witness_witness_left
40Separate the logical casesL160–163

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

  1. L160
    cases hinner
  2. L161
    cases hinner_right
  3. L162
    cases hinner_right_right
  4. L163
    split
41Calculate and transport equalitiesL164–164

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

  1. L164
    trans x5 * x1 + x3
42Use earlier factsL165–165

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

  1. L165
    exact hleft_witness_witness_witness_witness_witness_witness_right_right_left
43Calculate and transport equalitiesL166–171

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

  1. L166
    trans x11 * x7 + x9
  2. L167
    rewrite hcell_left
  3. L168
    rewrite hinner_left
  4. L169
    rewrite hinner_right_right_left
  5. L170
    refl
  6. L171
    symm
44Use earlier factsL172–172

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

  1. L172
    exact hright_witness_witness_witness_witness_witness_witness_right_right_left
45Separate the logical casesL173–173

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

  1. L173
    split
46Calculate and transport equalitiesL174–174

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

  1. L174
    trans x5 * x2 + x4
47Use earlier factsL175–175

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

  1. L175
    exact hleft_witness_witness_witness_witness_witness_witness_right_right_right_left
48Calculate and transport equalitiesL176–181

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

  1. L176
    trans x11 * x8 + x10
  2. L177
    rewrite hcell_left
  3. L178
    rewrite hinner_right_left
  4. L179
    rewrite hinner_right_right_right
  5. L180
    refl
  6. L181
    symm
49Use earlier factsL182–182

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

  1. L182
    exact hright_witness_witness_witness_witness_witness_witness_right_right_right_left
50Separate the logical casesL183–183

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

  1. L183
    split
51Calculate and transport equalitiesL184–184

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

  1. L184
    trans x1
52Use earlier factsL185–185

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

  1. L185
    exact hleft_witness_witness_witness_witness_witness_witness_right_right_right_right_left
53Calculate and transport equalitiesL186–186

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

  1. L186
    trans x7
54Use earlier factsL187–187

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

  1. L187
    exact hinner_left
55Calculate and transport equalitiesL188–188

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

  1. L188
    symm
56Use earlier factsL189–189

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

  1. L189
    exact hright_witness_witness_witness_witness_witness_witness_right_right_right_right_left
57Calculate and transport equalitiesL190–190

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

  1. L190
    trans x2
58Use earlier factsL191–191

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

  1. L191
    exact hleft_witness_witness_witness_witness_witness_witness_right_right_right_right_right
59Calculate and transport equalitiesL192–192

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

  1. L192
    trans x8
60Use earlier factsL193–193

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

  1. L193
    exact hinner_right_left
61Calculate and transport equalitiesL194–194

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

  1. L194
    symm
62Use earlier factsL195–195

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

  1. L195
    exact hright_witness_witness_witness_witness_witness_witness_right_right_right_right_right

Library-wide reading audit

Original defined command ledger · 195 lines
  1. 0001induction k
  2. 0002intro s
  3. 0003intro h
  4. 0004intro e
  5. 0005intro H
  6. 0006intro E
  7. 0007intro u
  8. 0008intro U
  9. 0009intro v
  10. 0010intro V
  11. 0011intro a
  12. 0012intro A
  13. 0013intro b
  14. 0014intro B
  15. 0015intro hfirst
  16. 0016intro hsecond
  17. 0017have hleft : ((u = 1) /\ ((U = 0) /\ ((v = 0) /\ (V = 1))))
  18. 0018specialize cf_convergent_matrix_empty_elimination (s)
  19. 0019specialize cf_convergent_matrix_empty_elimination (h)
  20. 0020specialize cf_convergent_matrix_empty_elimination (e)
  21. 0021specialize cf_convergent_matrix_empty_elimination (u)
  22. 0022specialize cf_convergent_matrix_empty_elimination (U)
  23. 0023specialize cf_convergent_matrix_empty_elimination (v)
  24. 0024specialize cf_convergent_matrix_empty_elimination (V)
  25. 0025apply cf_convergent_matrix_empty_elimination
  26. 0026exact hfirst
  27. 0027have hright : ((a = 1) /\ ((A = 0) /\ ((b = 0) /\ (B = 1))))
  28. 0028specialize cf_convergent_matrix_empty_elimination (s)
  29. 0029specialize cf_convergent_matrix_empty_elimination (H)
  30. 0030specialize cf_convergent_matrix_empty_elimination (E)
  31. 0031specialize cf_convergent_matrix_empty_elimination (a)
  32. 0032specialize cf_convergent_matrix_empty_elimination (A)
  33. 0033specialize cf_convergent_matrix_empty_elimination (b)
  34. 0034specialize cf_convergent_matrix_empty_elimination (B)
  35. 0035apply cf_convergent_matrix_empty_elimination
  36. 0036exact hsecond
  37. 0037cases hleft
  38. 0038cases hleft_right
  39. 0039cases hleft_right_right
  40. 0040cases hright
  41. 0041cases hright_right
  42. 0042cases hright_right_right
  43. 0043split
  44. 0044trans 1
  45. 0045exact hleft_left
  46. 0046symm
  47. 0047exact hright_left
  48. 0048split
  49. 0049trans 0
  50. 0050exact hleft_right_left
  51. 0051symm
  52. 0052exact hright_right_left
  53. 0053split
  54. 0054trans 0
  55. 0055exact hleft_right_right_left
  56. 0056symm
  57. 0057exact hright_right_right_left
  58. 0058trans 1
  59. 0059exact hleft_right_right_right
  60. 0060symm
  61. 0061exact hright_right_right_right
  62. 0062intro s
  63. 0063intro h
  64. 0064intro e
  65. 0065intro H
  66. 0066intro E
  67. 0067intro u
  68. 0068intro U
  69. 0069intro v
  70. 0070intro V
  71. 0071intro a
  72. 0072intro A
  73. 0073intro b
  74. 0074intro B
  75. 0075intro hfirst
  76. 0076intro hsecond
  77. 0077have hleft : ∃ cfc_tail_functional_left. ∃ cfc_a_functional_left. ∃ cfc_b_functional_left. ∃ cfc_c_functional_left. ∃ cfc_d_functional_left. ∃ cfc_q_functional_left. ConvergentMatrixTrace(cfc_tail_functional_left,h,e,k,cfc_a_functional_left,cfc_b_functional_left,cfc_c_functional_left,cfc_d_functional_left) ∧ (ListCell(s,cfc_q_functional_left,cfc_tail_functional_left) ∧ (u = cfc_q_functional_left · cfc_a_functional_left + cfc_c_functional_left ∧ (U = cfc_q_functional_left · cfc_b_functional_left + cfc_d_functional_left ∧ (v = cfc_a_functional_left ∧ V = cfc_b_functional_left))))
  78. 0078specialize cf_convergent_matrix_successor_elimination (s)
  79. 0079specialize cf_convergent_matrix_successor_elimination (h)
  80. 0080specialize cf_convergent_matrix_successor_elimination (e)
  81. 0081specialize cf_convergent_matrix_successor_elimination (k)
  82. 0082specialize cf_convergent_matrix_successor_elimination (u)
  83. 0083specialize cf_convergent_matrix_successor_elimination (U)
  84. 0084specialize cf_convergent_matrix_successor_elimination (v)
  85. 0085specialize cf_convergent_matrix_successor_elimination (V)
  86. 0086apply cf_convergent_matrix_successor_elimination
  87. 0087exact hfirst
  88. 0088have hright : ∃ cfc_tail_functional_right. ∃ cfc_a_functional_right. ∃ cfc_b_functional_right. ∃ cfc_c_functional_right. ∃ cfc_d_functional_right. ∃ cfc_q_functional_right. ConvergentMatrixTrace(cfc_tail_functional_right,H,E,k,cfc_a_functional_right,cfc_b_functional_right,cfc_c_functional_right,cfc_d_functional_right) ∧ (ListCell(s,cfc_q_functional_right,cfc_tail_functional_right) ∧ (a = cfc_q_functional_right · cfc_a_functional_right + cfc_c_functional_right ∧ (A = cfc_q_functional_right · cfc_b_functional_right + cfc_d_functional_right ∧ (b = cfc_a_functional_right ∧ B = cfc_b_functional_right))))
  89. 0089specialize cf_convergent_matrix_successor_elimination (s)
  90. 0090specialize cf_convergent_matrix_successor_elimination (H)
  91. 0091specialize cf_convergent_matrix_successor_elimination (E)
  92. 0092specialize cf_convergent_matrix_successor_elimination (k)
  93. 0093specialize cf_convergent_matrix_successor_elimination (a)
  94. 0094specialize cf_convergent_matrix_successor_elimination (A)
  95. 0095specialize cf_convergent_matrix_successor_elimination (b)
  96. 0096specialize cf_convergent_matrix_successor_elimination (B)
  97. 0097apply cf_convergent_matrix_successor_elimination
  98. 0098exact hsecond
  99. 0099cases hleft
  100. 0100cases hleft_witness
  101. 0101cases hleft_witness_witness
  102. 0102cases hleft_witness_witness_witness
  103. 0103cases hleft_witness_witness_witness_witness
  104. 0104cases hleft_witness_witness_witness_witness_witness
  105. 0105cases hright
  106. 0106cases hright_witness
  107. 0107cases hright_witness_witness
  108. 0108cases hright_witness_witness_witness
  109. 0109cases hright_witness_witness_witness_witness
  110. 0110cases hright_witness_witness_witness_witness_witness
  111. 0111cases hleft_witness_witness_witness_witness_witness_witness
  112. 0112cases hleft_witness_witness_witness_witness_witness_witness_right
  113. 0113cases hleft_witness_witness_witness_witness_witness_witness_right_right
  114. 0114cases hleft_witness_witness_witness_witness_witness_witness_right_right_right
  115. 0115cases hleft_witness_witness_witness_witness_witness_witness_right_right_right_right
  116. 0116cases hright_witness_witness_witness_witness_witness_witness
  117. 0117cases hright_witness_witness_witness_witness_witness_witness_right
  118. 0118cases hright_witness_witness_witness_witness_witness_witness_right_right
  119. 0119cases hright_witness_witness_witness_witness_witness_witness_right_right_right
  120. 0120cases hright_witness_witness_witness_witness_witness_witness_right_right_right_right
  121. 0121have hcell : x5 = x11 /\ x = x6
  122. 0122specialize cell_functional (s)
  123. 0123specialize cell_functional (x5)
  124. 0124specialize cell_functional (x)
  125. 0125specialize cell_functional (x11)
  126. 0126specialize cell_functional (x6)
  127. 0127apply cell_functional
  128. 0128exact hleft_witness_witness_witness_witness_witness_witness_right_left
  129. 0129exact hright_witness_witness_witness_witness_witness_witness_right_left
  130. 0130cases hcell
  131. 0131have hinner : ((x1 = x7) /\ ((x2 = x8) /\ ((x3 = x9) /\ (x4 = x10))))
  132. 0132specialize IH (x)
  133. 0133specialize IH (h)
  134. 0134specialize IH (e)
  135. 0135specialize IH (H)
  136. 0136specialize IH (E)
  137. 0137specialize IH (x1)
  138. 0138specialize IH (x2)
  139. 0139specialize IH (x3)
  140. 0140specialize IH (x4)
  141. 0141specialize IH (x7)
  142. 0142specialize IH (x8)
  143. 0143specialize IH (x9)
  144. 0144specialize IH (x10)
  145. 0145apply IH
  146. 0146exact hleft_witness_witness_witness_witness_witness_witness_left
  147. 0147specialize cf_convergent_matrix_list_transport (x6)
  148. 0148specialize cf_convergent_matrix_list_transport (x)
  149. 0149specialize cf_convergent_matrix_list_transport (H)
  150. 0150specialize cf_convergent_matrix_list_transport (E)
  151. 0151specialize cf_convergent_matrix_list_transport (k)
  152. 0152specialize cf_convergent_matrix_list_transport (x7)
  153. 0153specialize cf_convergent_matrix_list_transport (x8)
  154. 0154specialize cf_convergent_matrix_list_transport (x9)
  155. 0155specialize cf_convergent_matrix_list_transport (x10)
  156. 0156apply cf_convergent_matrix_list_transport
  157. 0157symm
  158. 0158exact hcell_right
  159. 0159exact hright_witness_witness_witness_witness_witness_witness_left
  160. 0160cases hinner
  161. 0161cases hinner_right
  162. 0162cases hinner_right_right
  163. 0163split
  164. 0164trans x5 * x1 + x3
  165. 0165exact hleft_witness_witness_witness_witness_witness_witness_right_right_left
  166. 0166trans x11 * x7 + x9
  167. 0167rewrite hcell_left
  168. 0168rewrite hinner_left
  169. 0169rewrite hinner_right_right_left
  170. 0170refl
  171. 0171symm
  172. 0172exact hright_witness_witness_witness_witness_witness_witness_right_right_left
  173. 0173split
  174. 0174trans x5 * x2 + x4
  175. 0175exact hleft_witness_witness_witness_witness_witness_witness_right_right_right_left
  176. 0176trans x11 * x8 + x10
  177. 0177rewrite hcell_left
  178. 0178rewrite hinner_right_left
  179. 0179rewrite hinner_right_right_right
  180. 0180refl
  181. 0181symm
  182. 0182exact hright_witness_witness_witness_witness_witness_witness_right_right_right_left
  183. 0183split
  184. 0184trans x1
  185. 0185exact hleft_witness_witness_witness_witness_witness_witness_right_right_right_right_left
  186. 0186trans x7
  187. 0187exact hinner_left
  188. 0188symm
  189. 0189exact hright_witness_witness_witness_witness_witness_witness_right_right_right_right_left
  190. 0190trans x2
  191. 0191exact hleft_witness_witness_witness_witness_witness_witness_right_right_right_right_right
  192. 0192trans x8
  193. 0193exact hinner_right_left
  194. 0194symm
  195. 0195exact hright_witness_witness_witness_witness_witness_witness_right_right_right_right_right