BA003B

cf_convergent_matrix_extend_preserved_prefix

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

Appending the actual first-quotient matrix step preserves every earlier computed state and every transition under a genuine beta-prefix recoding.

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 t h e k u U v V q s H E. (exists cfc_tail_extend_old. ((exists cfc_state_extend_oldinitial. ((exists cfc_left_extend_oldinitialcode cfc_right_extend_oldinitialcode cfc_matrix_extend_oldinitialcode. ((cfc_left_extend_oldinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_extend_oldinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_extend_oldinitialcode = ((cfc_left_extend_oldinitialcode) + (cfc_right_extend_oldinitialcode)) * S ((cfc_left_extend_oldinitialcode) + (cfc_right_extend_oldinitialcode)) + ((cfc_right_extend_oldinitialcode) + (cfc_right_extend_oldinitialcode))) /\ ((cfc_state_extend_oldinitial) = ((cfc_tail_extend_old) + (cfc_matrix_extend_oldinitialcode)) * S ((cfc_tail_extend_old) + (cfc_matrix_extend_oldinitialcode)) + ((cfc_matrix_extend_oldinitialcode) + (cfc_matrix_extend_oldinitialcode))))))) /\ (((exists ff_h_extend_oldinitialentry. ff_h_extend_oldinitialentry + S (cfc_state_extend_oldinitial) = S ((S (0)) * e)) /\ exists ff_q_extend_oldinitialentry. h = ff_q_extend_oldinitialentry * S ((S (0)) * e) + (cfc_state_extend_oldinitial))))) /\ ((exists cfc_state_extend_oldterminal. ((exists cfc_left_extend_oldterminalcode cfc_right_extend_oldterminalcode cfc_matrix_extend_oldterminalcode. ((cfc_left_extend_oldterminalcode = ((u) + (U)) * S ((u) + (U)) + ((U) + (U))) /\ ((cfc_right_extend_oldterminalcode = ((v) + (V)) * S ((v) + (V)) + ((V) + (V))) /\ ((cfc_matrix_extend_oldterminalcode = ((cfc_left_extend_oldterminalcode) + (cfc_right_extend_oldterminalcode)) * S ((cfc_left_extend_oldterminalcode) + (cfc_right_extend_oldterminalcode)) + ((cfc_right_extend_oldterminalcode) + (cfc_right_extend_oldterminalcode))) /\ ((cfc_state_extend_oldterminal) = ((t) + (cfc_matrix_extend_oldterminalcode)) * S ((t) + (cfc_matrix_extend_oldterminalcode)) + ((cfc_matrix_extend_oldterminalcode) + (cfc_matrix_extend_oldterminalcode))))))) /\ (((exists ff_h_extend_oldterminalentry. ff_h_extend_oldterminalentry + S (cfc_state_extend_oldterminal) = S ((S (k)) * e)) /\ exists ff_q_extend_oldterminalentry. h = ff_q_extend_oldterminalentry * S ((S (k)) * e) + (cfc_state_extend_oldterminal))))) /\ (forall cfc_index_extend_old. (exists cfba_gap_extend_oldbound. cfba_gap_extend_oldbound + S (cfc_index_extend_old) = (k)) -> exists cfc_old_extend_old cfc_a_extend_old cfc_b_extend_old cfc_c_extend_old cfc_d_extend_old cfc_new_extend_old cfc_quotient_extend_old. ((exists cfc_state_extend_oldprevious. ((exists cfc_left_extend_oldpreviouscode cfc_right_extend_oldpreviouscode cfc_matrix_extend_oldpreviouscode. ((cfc_left_extend_oldpreviouscode = ((cfc_a_extend_old) + (cfc_b_extend_old)) * S ((cfc_a_extend_old) + (cfc_b_extend_old)) + ((cfc_b_extend_old) + (cfc_b_extend_old))) /\ ((cfc_right_extend_oldpreviouscode = ((cfc_c_extend_old) + (cfc_d_extend_old)) * S ((cfc_c_extend_old) + (cfc_d_extend_old)) + ((cfc_d_extend_old) + (cfc_d_extend_old))) /\ ((cfc_matrix_extend_oldpreviouscode = ((cfc_left_extend_oldpreviouscode) + (cfc_right_extend_oldpreviouscode)) * S ((cfc_left_extend_oldpreviouscode) + (cfc_right_extend_oldpreviouscode)) + ((cfc_right_extend_oldpreviouscode) + (cfc_right_extend_oldpreviouscode))) /\ ((cfc_state_extend_oldprevious) = ((cfc_old_extend_old) + (cfc_matrix_extend_oldpreviouscode)) * S ((cfc_old_extend_old) + (cfc_matrix_extend_oldpreviouscode)) + ((cfc_matrix_extend_oldpreviouscode) + (cfc_matrix_extend_oldpreviouscode))))))) /\ (((exists ff_h_extend_oldpreviousentry. ff_h_extend_oldpreviousentry + S (cfc_state_extend_oldprevious) = S ((S (cfc_index_extend_old)) * e)) /\ exists ff_q_extend_oldpreviousentry. h = ff_q_extend_oldpreviousentry * S ((S (cfc_index_extend_old)) * e) + (cfc_state_extend_oldprevious))))) /\ ((exists cfc_state_extend_oldfollowing. ((exists cfc_left_extend_oldfollowingcode cfc_right_extend_oldfollowingcode cfc_matrix_extend_oldfollowingcode. ((cfc_left_extend_oldfollowingcode = (((cfc_quotient_extend_old * cfc_a_extend_old + cfc_c_extend_old)) + ((cfc_quotient_extend_old * cfc_b_extend_old + cfc_d_extend_old))) * S (((cfc_quotient_extend_old * cfc_a_extend_old + cfc_c_extend_old)) + ((cfc_quotient_extend_old * cfc_b_extend_old + cfc_d_extend_old))) + (((cfc_quotient_extend_old * cfc_b_extend_old + cfc_d_extend_old)) + ((cfc_quotient_extend_old * cfc_b_extend_old + cfc_d_extend_old)))) /\ ((cfc_right_extend_oldfollowingcode = ((cfc_a_extend_old) + (cfc_b_extend_old)) * S ((cfc_a_extend_old) + (cfc_b_extend_old)) + ((cfc_b_extend_old) + (cfc_b_extend_old))) /\ ((cfc_matrix_extend_oldfollowingcode = ((cfc_left_extend_oldfollowingcode) + (cfc_right_extend_oldfollowingcode)) * S ((cfc_left_extend_oldfollowingcode) + (cfc_right_extend_oldfollowingcode)) + ((cfc_right_extend_oldfollowingcode) + (cfc_right_extend_oldfollowingcode))) /\ ((cfc_state_extend_oldfollowing) = ((cfc_new_extend_old) + (cfc_matrix_extend_oldfollowingcode)) * S ((cfc_new_extend_old) + (cfc_matrix_extend_oldfollowingcode)) + ((cfc_matrix_extend_oldfollowingcode) + (cfc_matrix_extend_oldfollowingcode))))))) /\ (((exists ff_h_extend_oldfollowingentry. ff_h_extend_oldfollowingentry + S (cfc_state_extend_oldfollowing) = S ((S (S cfc_index_extend_old)) * e)) /\ exists ff_q_extend_oldfollowingentry. h = ff_q_extend_oldfollowingentry * S ((S (S cfc_index_extend_old)) * e) + (cfc_state_extend_oldfollowing))))) /\ (cfc_new_extend_old = S ((cfc_quotient_extend_old + cfc_old_extend_old) * S (cfc_quotient_extend_old + cfc_old_extend_old) + (cfc_old_extend_old + cfc_old_extend_old))))))))) -> (s = S ((q + t) * S (q + t) + (t + t))) -> (exists cfc_state_extend_new_state. ((exists cfc_left_extend_new_statecode cfc_right_extend_new_statecode cfc_matrix_extend_new_statecode. ((cfc_left_extend_new_statecode = (((q * u + v)) + ((q * U + V))) * S (((q * u + v)) + ((q * U + V))) + (((q * U + V)) + ((q * U + V)))) /\ ((cfc_right_extend_new_statecode = ((u) + (U)) * S ((u) + (U)) + ((U) + (U))) /\ ((cfc_matrix_extend_new_statecode = ((cfc_left_extend_new_statecode) + (cfc_right_extend_new_statecode)) * S ((cfc_left_extend_new_statecode) + (cfc_right_extend_new_statecode)) + ((cfc_right_extend_new_statecode) + (cfc_right_extend_new_statecode))) /\ ((cfc_state_extend_new_state) = ((s) + (cfc_matrix_extend_new_statecode)) * S ((s) + (cfc_matrix_extend_new_statecode)) + ((cfc_matrix_extend_new_statecode) + (cfc_matrix_extend_new_statecode))))))) /\ (((exists ff_h_extend_new_stateentry. ff_h_extend_new_stateentry + S (cfc_state_extend_new_state) = S ((S (S k)) * E)) /\ exists ff_q_extend_new_stateentry. H = ff_q_extend_new_stateentry * S ((S (S k)) * E) + (cfc_state_extend_new_state))))) -> (forall cfc_index_extend_preserves cfc_value_extend_preserves. (exists cfba_gap_extend_preservesbound. cfba_gap_extend_preservesbound + S (cfc_index_extend_preserves) = (S k)) -> (((exists ff_h_extend_preservessource. ff_h_extend_preservessource + S (cfc_value_extend_preserves) = S ((S (cfc_index_extend_preserves)) * e)) /\ exists ff_q_extend_preservessource. h = ff_q_extend_preservessource * S ((S (cfc_index_extend_preserves)) * e) + (cfc_value_extend_preserves))) -> (((exists ff_h_extend_preservestarget. ff_h_extend_preservestarget + S (cfc_value_extend_preserves) = S ((S (cfc_index_extend_preserves)) * E)) /\ exists ff_q_extend_preservestarget. H = ff_q_extend_preservestarget * S ((S (cfc_index_extend_preserves)) * E) + (cfc_value_extend_preserves)))) -> (exists cfc_tail_extend_result. ((exists cfc_state_extend_resultinitial. ((exists cfc_left_extend_resultinitialcode cfc_right_extend_resultinitialcode cfc_matrix_extend_resultinitialcode. ((cfc_left_extend_resultinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_extend_resultinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_extend_resultinitialcode = ((cfc_left_extend_resultinitialcode) + (cfc_right_extend_resultinitialcode)) * S ((cfc_left_extend_resultinitialcode) + (cfc_right_extend_resultinitialcode)) + ((cfc_right_extend_resultinitialcode) + (cfc_right_extend_resultinitialcode))) /\ ((cfc_state_extend_resultinitial) = ((cfc_tail_extend_result) + (cfc_matrix_extend_resultinitialcode)) * S ((cfc_tail_extend_result) + (cfc_matrix_extend_resultinitialcode)) + ((cfc_matrix_extend_resultinitialcode) + (cfc_matrix_extend_resultinitialcode))))))) /\ (((exists ff_h_extend_resultinitialentry. ff_h_extend_resultinitialentry + S (cfc_state_extend_resultinitial) = S ((S (0)) * E)) /\ exists ff_q_extend_resultinitialentry. H = ff_q_extend_resultinitialentry * S ((S (0)) * E) + (cfc_state_extend_resultinitial))))) /\ ((exists cfc_state_extend_resultterminal. ((exists cfc_left_extend_resultterminalcode cfc_right_extend_resultterminalcode cfc_matrix_extend_resultterminalcode. ((cfc_left_extend_resultterminalcode = (((q * u + v)) + ((q * U + V))) * S (((q * u + v)) + ((q * U + V))) + (((q * U + V)) + ((q * U + V)))) /\ ((cfc_right_extend_resultterminalcode = ((u) + (U)) * S ((u) + (U)) + ((U) + (U))) /\ ((cfc_matrix_extend_resultterminalcode = ((cfc_left_extend_resultterminalcode) + (cfc_right_extend_resultterminalcode)) * S ((cfc_left_extend_resultterminalcode) + (cfc_right_extend_resultterminalcode)) + ((cfc_right_extend_resultterminalcode) + (cfc_right_extend_resultterminalcode))) /\ ((cfc_state_extend_resultterminal) = ((s) + (cfc_matrix_extend_resultterminalcode)) * S ((s) + (cfc_matrix_extend_resultterminalcode)) + ((cfc_matrix_extend_resultterminalcode) + (cfc_matrix_extend_resultterminalcode))))))) /\ (((exists ff_h_extend_resultterminalentry. ff_h_extend_resultterminalentry + S (cfc_state_extend_resultterminal) = S ((S (S k)) * E)) /\ exists ff_q_extend_resultterminalentry. H = ff_q_extend_resultterminalentry * S ((S (S k)) * E) + (cfc_state_extend_resultterminal))))) /\ (forall cfc_index_extend_result. (exists cfba_gap_extend_resultbound. cfba_gap_extend_resultbound + S (cfc_index_extend_result) = (S k)) -> exists cfc_old_extend_result cfc_a_extend_result cfc_b_extend_result cfc_c_extend_result cfc_d_extend_result cfc_new_extend_result cfc_quotient_extend_result. ((exists cfc_state_extend_resultprevious. ((exists cfc_left_extend_resultpreviouscode cfc_right_extend_resultpreviouscode cfc_matrix_extend_resultpreviouscode. ((cfc_left_extend_resultpreviouscode = ((cfc_a_extend_result) + (cfc_b_extend_result)) * S ((cfc_a_extend_result) + (cfc_b_extend_result)) + ((cfc_b_extend_result) + (cfc_b_extend_result))) /\ ((cfc_right_extend_resultpreviouscode = ((cfc_c_extend_result) + (cfc_d_extend_result)) * S ((cfc_c_extend_result) + (cfc_d_extend_result)) + ((cfc_d_extend_result) + (cfc_d_extend_result))) /\ ((cfc_matrix_extend_resultpreviouscode = ((cfc_left_extend_resultpreviouscode) + (cfc_right_extend_resultpreviouscode)) * S ((cfc_left_extend_resultpreviouscode) + (cfc_right_extend_resultpreviouscode)) + ((cfc_right_extend_resultpreviouscode) + (cfc_right_extend_resultpreviouscode))) /\ ((cfc_state_extend_resultprevious) = ((cfc_old_extend_result) + (cfc_matrix_extend_resultpreviouscode)) * S ((cfc_old_extend_result) + (cfc_matrix_extend_resultpreviouscode)) + ((cfc_matrix_extend_resultpreviouscode) + (cfc_matrix_extend_resultpreviouscode))))))) /\ (((exists ff_h_extend_resultpreviousentry. ff_h_extend_resultpreviousentry + S (cfc_state_extend_resultprevious) = S ((S (cfc_index_extend_result)) * E)) /\ exists ff_q_extend_resultpreviousentry. H = ff_q_extend_resultpreviousentry * S ((S (cfc_index_extend_result)) * E) + (cfc_state_extend_resultprevious))))) /\ ((exists cfc_state_extend_resultfollowing. ((exists cfc_left_extend_resultfollowingcode cfc_right_extend_resultfollowingcode cfc_matrix_extend_resultfollowingcode. ((cfc_left_extend_resultfollowingcode = (((cfc_quotient_extend_result * cfc_a_extend_result + cfc_c_extend_result)) + ((cfc_quotient_extend_result * cfc_b_extend_result + cfc_d_extend_result))) * S (((cfc_quotient_extend_result * cfc_a_extend_result + cfc_c_extend_result)) + ((cfc_quotient_extend_result * cfc_b_extend_result + cfc_d_extend_result))) + (((cfc_quotient_extend_result * cfc_b_extend_result + cfc_d_extend_result)) + ((cfc_quotient_extend_result * cfc_b_extend_result + cfc_d_extend_result)))) /\ ((cfc_right_extend_resultfollowingcode = ((cfc_a_extend_result) + (cfc_b_extend_result)) * S ((cfc_a_extend_result) + (cfc_b_extend_result)) + ((cfc_b_extend_result) + (cfc_b_extend_result))) /\ ((cfc_matrix_extend_resultfollowingcode = ((cfc_left_extend_resultfollowingcode) + (cfc_right_extend_resultfollowingcode)) * S ((cfc_left_extend_resultfollowingcode) + (cfc_right_extend_resultfollowingcode)) + ((cfc_right_extend_resultfollowingcode) + (cfc_right_extend_resultfollowingcode))) /\ ((cfc_state_extend_resultfollowing) = ((cfc_new_extend_result) + (cfc_matrix_extend_resultfollowingcode)) * S ((cfc_new_extend_result) + (cfc_matrix_extend_resultfollowingcode)) + ((cfc_matrix_extend_resultfollowingcode) + (cfc_matrix_extend_resultfollowingcode))))))) /\ (((exists ff_h_extend_resultfollowingentry. ff_h_extend_resultfollowingentry + S (cfc_state_extend_resultfollowing) = S ((S (S cfc_index_extend_result)) * E)) /\ exists ff_q_extend_resultfollowingentry. H = ff_q_extend_resultfollowingentry * S ((S (S cfc_index_extend_result)) * E) + (cfc_state_extend_resultfollowing))))) /\ (cfc_new_extend_result = S ((cfc_quotient_extend_result + cfc_old_extend_result) * S (cfc_quotient_extend_result + cfc_old_extend_result) + (cfc_old_extend_result + cfc_old_extend_result)))))))))

Constructive proof overview

Generated structural guide

Appending the actual first-quotient matrix step preserves every earlier computed state and every transition under a genuine beta-prefix recoding.

The unchanged tactic script uses 5 declared prerequisites and contains 139 exact native proof lines.

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

Proof neighborhood

Direct dependencies

BA0038 cf_convergent_matrix_state_prefix_transport le_of_succ_le_succ Stable theorem; checked-use authorized le_eq_or_lt Stable theorem; checked-use authorized zero_add Stable theorem; checked-use authorized succ_le_succ Stable theorem; checked-use authorized

Direct dependents

BA003C cf_convergent_matrix_prepend_exists

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

139 script commands · 34 reading checkpoints · 3 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 prefix transport

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 t
  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 q
  10. L10
    intro s
02Fix variables and assumptionsL11–16

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

  1. L11
    intro H
  2. L12
    intro E
  3. L13
    intro ht
  4. L14
    intro hcell
  5. L15
    intro hnew
  6. L16
    intro hp
03Separate the logical casesL17–19

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

  1. L17
    cases ht
  2. L18
    cases ht_witness
  3. L19
    cases ht_witness_right
04Construct an explicit witnessL20–20

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

  1. L20
    exists x
05Separate the logical casesL21–21

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

  1. L21
    split
06Use earlier factsL22–31

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

  1. L22
    specialize cf_convergent_matrix_state_prefix_transport (h)
  2. L23
    specialize cf_convergent_matrix_state_prefix_transport (e)
  3. L24
    specialize cf_convergent_matrix_state_prefix_transport (H)
  4. L25
    specialize cf_convergent_matrix_state_prefix_transport (E)
  5. L26
    specialize cf_convergent_matrix_state_prefix_transport (S k)
  6. L27
    specialize cf_convergent_matrix_state_prefix_transport (0)
  7. L28
    specialize cf_convergent_matrix_state_prefix_transport (x)
  8. L29
    specialize cf_convergent_matrix_state_prefix_transport (1)
  9. L30
    specialize cf_convergent_matrix_state_prefix_transport (0)
  10. L31
    specialize cf_convergent_matrix_state_prefix_transport (0)
07Use earlier factsL32–34

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

  1. L32
    specialize cf_convergent_matrix_state_prefix_transport (1)
  2. L33
    apply cf_convergent_matrix_state_prefix_transport
  3. L34
    exact hp
08Construct an explicit witnessL35–35

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

  1. L35
    exists k
09Calculate and transport equalitiesL36–36

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

  1. L36
    simp
10Use earlier factsL37–37

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

  1. L37
    exact ht_witness_left
11Separate the logical casesL38–38

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

  1. L38
    split
12Use earlier factsL39–39

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

  1. L39
    exact hnew
13Fix variables and assumptionsL40–41

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

  1. L40
    intro j
  2. L41
    intro hj
14Establish hjkL42–46

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

  1. L42
    have hjk : exists cfba_bound_extend_index. cfba_bound_extend_index + (j) = (k)
  2. L43
    specialize le_of_succ_le_succ (j)
  3. L44
    specialize le_of_succ_le_succ (k)
  4. L45
    apply le_of_succ_le_succ
  5. L46
    exact hj
15Establish heqL47–51

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le eq or lt.

  1. L47
    have heq : j = k \/ (exists cfba_gap_extend_case. cfba_gap_extend_case + S (j) = (k))
  2. L48
    specialize le_eq_or_lt (j)
  3. L49
    specialize le_eq_or_lt (k)
  4. L50
    apply le_eq_or_lt
  5. L51
    exact hjk
16Separate the logical casesL52–52

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

  1. L52
    cases heq
17Calculate and transport equalitiesL53–56

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

  1. L53
    rewrite heq_left
  2. L54
    rewrite heq_left
  3. L55
    rewrite heq_left
  4. L56
    rewrite heq_left
18Construct an explicit witnessL57–63

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

  1. L57
    exists t
  2. L58
    exists u
  3. L59
    exists U
  4. L60
    exists v
  5. L61
    exists V
  6. L62
    exists s
  7. L63
    exists q
19Separate the logical casesL64–64

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

  1. L64
    split
20Use earlier factsL65–74

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

  1. L65
    specialize cf_convergent_matrix_state_prefix_transport (h)
  2. L66
    specialize cf_convergent_matrix_state_prefix_transport (e)
  3. L67
    specialize cf_convergent_matrix_state_prefix_transport (H)
  4. L68
    specialize cf_convergent_matrix_state_prefix_transport (E)
  5. L69
    specialize cf_convergent_matrix_state_prefix_transport (S k)
  6. L70
    specialize cf_convergent_matrix_state_prefix_transport (k)
  7. L71
    specialize cf_convergent_matrix_state_prefix_transport (t)
  8. L72
    specialize cf_convergent_matrix_state_prefix_transport (u)
  9. L73
    specialize cf_convergent_matrix_state_prefix_transport (U)
  10. L74
    specialize cf_convergent_matrix_state_prefix_transport (v)
21Use earlier factsL75–77

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

  1. L75
    specialize cf_convergent_matrix_state_prefix_transport (V)
  2. L76
    apply cf_convergent_matrix_state_prefix_transport
  3. L77
    exact hp
22Construct an explicit witnessL78–78

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

  1. L78
    exists 0
23Use earlier factsL79–80

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

  1. L79
    apply zero_add
  2. L80
    exact ht_witness_right_left
24Separate the logical casesL81–81

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

  1. L81
    split
25Use earlier factsL82–83

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

  1. L82
    exact hnew
  2. L83
    exact hcell
26Establish hsL84–87

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

  1. L84
    have hs · expand full local formula (768 characters)have hs : ∃ cfc_old_extend_previous_step. ∃ cfc_a_extend_previous_step. ∃ cfc_b_extend_previous_step. ∃ cfc_c_extend_previous_step. ∃ cfc_d_extend_previous_step. ∃ cfc_new_extend_previous_step. ∃ cfc_q_extend_previous_step. ConvergentMatrixAt(h,e,j,cfc_old_extend_previous_step,cfc_a_extend_previous_step,cfc_b_extend_previous_step,cfc_c_extend_previous_step,cfc_d_extend_previous_step) ∧ (ConvergentMatrixAt(h,e,S j,cfc_new_extend_previous_step,cfc_q_extend_previous_step · cfc_a_extend_previous_step + cfc_c_extend_previous_step,cfc_q_extend_previous_step · cfc_b_extend_previous_step + cfc_d_extend_previous_step,cfc_a_extend_previous_step,cfc_b_extend_previous_step) ∧ ListCell(cfc_new_extend_previous_step,cfc_q_extend_previous_step,cfc_old_extend_previous_step))
    Definitions: ListCellConvergentMatrixAt
  2. L85
    specialize ht_witness_right_right (j)
  3. L86
    apply ht_witness_right_right
  4. L87
    exact heq_right
27Separate the logical casesL88–96

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

  1. L88
    cases hs
  2. L89
    cases hs_witness
  3. L90
    cases hs_witness_witness
  4. L91
    cases hs_witness_witness_witness
  5. L92
    cases hs_witness_witness_witness_witness
  6. L93
    cases hs_witness_witness_witness_witness_witness
  7. L94
    cases hs_witness_witness_witness_witness_witness_witness
  8. L95
    cases hs_witness_witness_witness_witness_witness_witness_witness
  9. L96
    cases hs_witness_witness_witness_witness_witness_witness_witness_right
28Construct an explicit witnessL97–103

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

  1. L97
    exists x1
  2. L98
    exists x2
  3. L99
    exists x3
  4. L100
    exists x4
  5. L101
    exists x5
  6. L102
    exists x6
  7. L103
    exists x7
29Separate the logical casesL104–104

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

  1. L104
    split
30Use earlier factsL105–114

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

  1. L105
    specialize cf_convergent_matrix_state_prefix_transport (h)
  2. L106
    specialize cf_convergent_matrix_state_prefix_transport (e)
  3. L107
    specialize cf_convergent_matrix_state_prefix_transport (H)
  4. L108
    specialize cf_convergent_matrix_state_prefix_transport (E)
  5. L109
    specialize cf_convergent_matrix_state_prefix_transport (S k)
  6. L110
    specialize cf_convergent_matrix_state_prefix_transport (j)
  7. L111
    specialize cf_convergent_matrix_state_prefix_transport (x1)
  8. L112
    specialize cf_convergent_matrix_state_prefix_transport (x2)
  9. L113
    specialize cf_convergent_matrix_state_prefix_transport (x3)
  10. L114
    specialize cf_convergent_matrix_state_prefix_transport (x4)
31Use earlier factsL115–119

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

  1. L115
    specialize cf_convergent_matrix_state_prefix_transport (x5)
  2. L116
    apply cf_convergent_matrix_state_prefix_transport
  3. L117
    exact hp
  4. L118
    exact hj
  5. L119
    exact hs_witness_witness_witness_witness_witness_witness_witness_left
32Separate the logical casesL120–120

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

  1. L120
    split
33Use earlier factsL121–130

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

  1. L121
    specialize cf_convergent_matrix_state_prefix_transport (h)
  2. L122
    specialize cf_convergent_matrix_state_prefix_transport (e)
  3. L123
    specialize cf_convergent_matrix_state_prefix_transport (H)
  4. L124
    specialize cf_convergent_matrix_state_prefix_transport (E)
  5. L125
    specialize cf_convergent_matrix_state_prefix_transport (S k)
  6. L126
    specialize cf_convergent_matrix_state_prefix_transport (S j)
  7. L127
    specialize cf_convergent_matrix_state_prefix_transport (x6)
  8. L128
    specialize cf_convergent_matrix_state_prefix_transport (x7 * x2 + x4)
  9. L129
    specialize cf_convergent_matrix_state_prefix_transport (x7 * x3 + x5)
  10. L130
    specialize cf_convergent_matrix_state_prefix_transport (x2)
34Use earlier factsL131–139

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

  1. L131
    specialize cf_convergent_matrix_state_prefix_transport (x3)
  2. L132
    apply cf_convergent_matrix_state_prefix_transport
  3. L133
    exact hp
  4. L134
    specialize succ_le_succ (S j)
  5. L135
    specialize succ_le_succ (k)
  6. L136
    apply succ_le_succ
  7. L137
    exact heq_right
  8. L138
    exact hs_witness_witness_witness_witness_witness_witness_witness_right_left
  9. L139
    exact hs_witness_witness_witness_witness_witness_witness_witness_right_right

Library-wide reading audit

Original exact command ledger · 139 lines
  1. 0001intro t
  2. 0002intro h
  3. 0003intro e
  4. 0004intro k
  5. 0005intro u
  6. 0006intro U
  7. 0007intro v
  8. 0008intro V
  9. 0009intro q
  10. 0010intro s
  11. 0011intro H
  12. 0012intro E
  13. 0013intro ht
  14. 0014intro hcell
  15. 0015intro hnew
  16. 0016intro hp
  17. 0017cases ht
  18. 0018cases ht_witness
  19. 0019cases ht_witness_right
  20. 0020exists x
  21. 0021split
  22. 0022specialize cf_convergent_matrix_state_prefix_transport (h)
  23. 0023specialize cf_convergent_matrix_state_prefix_transport (e)
  24. 0024specialize cf_convergent_matrix_state_prefix_transport (H)
  25. 0025specialize cf_convergent_matrix_state_prefix_transport (E)
  26. 0026specialize cf_convergent_matrix_state_prefix_transport (S k)
  27. 0027specialize cf_convergent_matrix_state_prefix_transport (0)
  28. 0028specialize cf_convergent_matrix_state_prefix_transport (x)
  29. 0029specialize cf_convergent_matrix_state_prefix_transport (1)
  30. 0030specialize cf_convergent_matrix_state_prefix_transport (0)
  31. 0031specialize cf_convergent_matrix_state_prefix_transport (0)
  32. 0032specialize cf_convergent_matrix_state_prefix_transport (1)
  33. 0033apply cf_convergent_matrix_state_prefix_transport
  34. 0034exact hp
  35. 0035exists k
  36. 0036simp
  37. 0037exact ht_witness_left
  38. 0038split
  39. 0039exact hnew
  40. 0040intro j
  41. 0041intro hj
  42. 0042have hjk : exists cfba_bound_extend_index. cfba_bound_extend_index + (j) = (k)
  43. 0043specialize le_of_succ_le_succ (j)
  44. 0044specialize le_of_succ_le_succ (k)
  45. 0045apply le_of_succ_le_succ
  46. 0046exact hj
  47. 0047have heq : j = k \/ (exists cfba_gap_extend_case. cfba_gap_extend_case + S (j) = (k))
  48. 0048specialize le_eq_or_lt (j)
  49. 0049specialize le_eq_or_lt (k)
  50. 0050apply le_eq_or_lt
  51. 0051exact hjk
  52. 0052cases heq
  53. 0053rewrite heq_left
  54. 0054rewrite heq_left
  55. 0055rewrite heq_left
  56. 0056rewrite heq_left
  57. 0057exists t
  58. 0058exists u
  59. 0059exists U
  60. 0060exists v
  61. 0061exists V
  62. 0062exists s
  63. 0063exists q
  64. 0064split
  65. 0065specialize cf_convergent_matrix_state_prefix_transport (h)
  66. 0066specialize cf_convergent_matrix_state_prefix_transport (e)
  67. 0067specialize cf_convergent_matrix_state_prefix_transport (H)
  68. 0068specialize cf_convergent_matrix_state_prefix_transport (E)
  69. 0069specialize cf_convergent_matrix_state_prefix_transport (S k)
  70. 0070specialize cf_convergent_matrix_state_prefix_transport (k)
  71. 0071specialize cf_convergent_matrix_state_prefix_transport (t)
  72. 0072specialize cf_convergent_matrix_state_prefix_transport (u)
  73. 0073specialize cf_convergent_matrix_state_prefix_transport (U)
  74. 0074specialize cf_convergent_matrix_state_prefix_transport (v)
  75. 0075specialize cf_convergent_matrix_state_prefix_transport (V)
  76. 0076apply cf_convergent_matrix_state_prefix_transport
  77. 0077exact hp
  78. 0078exists 0
  79. 0079apply zero_add
  80. 0080exact ht_witness_right_left
  81. 0081split
  82. 0082exact hnew
  83. 0083exact hcell
  84. 0084have hs : exists cfc_old_extend_previous_step cfc_a_extend_previous_step cfc_b_extend_previous_step cfc_c_extend_previous_step cfc_d_extend_previous_step cfc_new_extend_previous_step cfc_q_extend_previous_step. ((exists cfc_state_extend_previous_stepprevious. ((exists cfc_left_extend_previous_steppreviouscode cfc_right_extend_previous_steppreviouscode cfc_matrix_extend_previous_steppreviouscode. ((cfc_left_extend_previous_steppreviouscode = ((cfc_a_extend_previous_step) + (cfc_b_extend_previous_step)) * S ((cfc_a_extend_previous_step) + (cfc_b_extend_previous_step)) + ((cfc_b_extend_previous_step) + (cfc_b_extend_previous_step))) /\ ((cfc_right_extend_previous_steppreviouscode = ((cfc_c_extend_previous_step) + (cfc_d_extend_previous_step)) * S ((cfc_c_extend_previous_step) + (cfc_d_extend_previous_step)) + ((cfc_d_extend_previous_step) + (cfc_d_extend_previous_step))) /\ ((cfc_matrix_extend_previous_steppreviouscode = ((cfc_left_extend_previous_steppreviouscode) + (cfc_right_extend_previous_steppreviouscode)) * S ((cfc_left_extend_previous_steppreviouscode) + (cfc_right_extend_previous_steppreviouscode)) + ((cfc_right_extend_previous_steppreviouscode) + (cfc_right_extend_previous_steppreviouscode))) /\ ((cfc_state_extend_previous_stepprevious) = ((cfc_old_extend_previous_step) + (cfc_matrix_extend_previous_steppreviouscode)) * S ((cfc_old_extend_previous_step) + (cfc_matrix_extend_previous_steppreviouscode)) + ((cfc_matrix_extend_previous_steppreviouscode) + (cfc_matrix_extend_previous_steppreviouscode))))))) /\ (((exists ff_h_extend_previous_steppreviousentry. ff_h_extend_previous_steppreviousentry + S (cfc_state_extend_previous_stepprevious) = S ((S (j)) * e)) /\ exists ff_q_extend_previous_steppreviousentry. h = ff_q_extend_previous_steppreviousentry * S ((S (j)) * e) + (cfc_state_extend_previous_stepprevious))))) /\ ((exists cfc_state_extend_previous_stepfollowing. ((exists cfc_left_extend_previous_stepfollowingcode cfc_right_extend_previous_stepfollowingcode cfc_matrix_extend_previous_stepfollowingcode. ((cfc_left_extend_previous_stepfollowingcode = (((cfc_q_extend_previous_step * cfc_a_extend_previous_step + cfc_c_extend_previous_step)) + ((cfc_q_extend_previous_step * cfc_b_extend_previous_step + cfc_d_extend_previous_step))) * S (((cfc_q_extend_previous_step * cfc_a_extend_previous_step + cfc_c_extend_previous_step)) + ((cfc_q_extend_previous_step * cfc_b_extend_previous_step + cfc_d_extend_previous_step))) + (((cfc_q_extend_previous_step * cfc_b_extend_previous_step + cfc_d_extend_previous_step)) + ((cfc_q_extend_previous_step * cfc_b_extend_previous_step + cfc_d_extend_previous_step)))) /\ ((cfc_right_extend_previous_stepfollowingcode = ((cfc_a_extend_previous_step) + (cfc_b_extend_previous_step)) * S ((cfc_a_extend_previous_step) + (cfc_b_extend_previous_step)) + ((cfc_b_extend_previous_step) + (cfc_b_extend_previous_step))) /\ ((cfc_matrix_extend_previous_stepfollowingcode = ((cfc_left_extend_previous_stepfollowingcode) + (cfc_right_extend_previous_stepfollowingcode)) * S ((cfc_left_extend_previous_stepfollowingcode) + (cfc_right_extend_previous_stepfollowingcode)) + ((cfc_right_extend_previous_stepfollowingcode) + (cfc_right_extend_previous_stepfollowingcode))) /\ ((cfc_state_extend_previous_stepfollowing) = ((cfc_new_extend_previous_step) + (cfc_matrix_extend_previous_stepfollowingcode)) * S ((cfc_new_extend_previous_step) + (cfc_matrix_extend_previous_stepfollowingcode)) + ((cfc_matrix_extend_previous_stepfollowingcode) + (cfc_matrix_extend_previous_stepfollowingcode))))))) /\ (((exists ff_h_extend_previous_stepfollowingentry. ff_h_extend_previous_stepfollowingentry + S (cfc_state_extend_previous_stepfollowing) = S ((S (S (j))) * e)) /\ exists ff_q_extend_previous_stepfollowingentry. h = ff_q_extend_previous_stepfollowingentry * S ((S (S (j))) * e) + (cfc_state_extend_previous_stepfollowing))))) /\ (cfc_new_extend_previous_step = S ((cfc_q_extend_previous_step + cfc_old_extend_previous_step) * S (cfc_q_extend_previous_step + cfc_old_extend_previous_step) + (cfc_old_extend_previous_step + cfc_old_extend_previous_step)))))
  85. 0085specialize ht_witness_right_right (j)
  86. 0086apply ht_witness_right_right
  87. 0087exact heq_right
  88. 0088cases hs
  89. 0089cases hs_witness
  90. 0090cases hs_witness_witness
  91. 0091cases hs_witness_witness_witness
  92. 0092cases hs_witness_witness_witness_witness
  93. 0093cases hs_witness_witness_witness_witness_witness
  94. 0094cases hs_witness_witness_witness_witness_witness_witness
  95. 0095cases hs_witness_witness_witness_witness_witness_witness_witness
  96. 0096cases hs_witness_witness_witness_witness_witness_witness_witness_right
  97. 0097exists x1
  98. 0098exists x2
  99. 0099exists x3
  100. 0100exists x4
  101. 0101exists x5
  102. 0102exists x6
  103. 0103exists x7
  104. 0104split
  105. 0105specialize cf_convergent_matrix_state_prefix_transport (h)
  106. 0106specialize cf_convergent_matrix_state_prefix_transport (e)
  107. 0107specialize cf_convergent_matrix_state_prefix_transport (H)
  108. 0108specialize cf_convergent_matrix_state_prefix_transport (E)
  109. 0109specialize cf_convergent_matrix_state_prefix_transport (S k)
  110. 0110specialize cf_convergent_matrix_state_prefix_transport (j)
  111. 0111specialize cf_convergent_matrix_state_prefix_transport (x1)
  112. 0112specialize cf_convergent_matrix_state_prefix_transport (x2)
  113. 0113specialize cf_convergent_matrix_state_prefix_transport (x3)
  114. 0114specialize cf_convergent_matrix_state_prefix_transport (x4)
  115. 0115specialize cf_convergent_matrix_state_prefix_transport (x5)
  116. 0116apply cf_convergent_matrix_state_prefix_transport
  117. 0117exact hp
  118. 0118exact hj
  119. 0119exact hs_witness_witness_witness_witness_witness_witness_witness_left
  120. 0120split
  121. 0121specialize cf_convergent_matrix_state_prefix_transport (h)
  122. 0122specialize cf_convergent_matrix_state_prefix_transport (e)
  123. 0123specialize cf_convergent_matrix_state_prefix_transport (H)
  124. 0124specialize cf_convergent_matrix_state_prefix_transport (E)
  125. 0125specialize cf_convergent_matrix_state_prefix_transport (S k)
  126. 0126specialize cf_convergent_matrix_state_prefix_transport (S j)
  127. 0127specialize cf_convergent_matrix_state_prefix_transport (x6)
  128. 0128specialize cf_convergent_matrix_state_prefix_transport (x7 * x2 + x4)
  129. 0129specialize cf_convergent_matrix_state_prefix_transport (x7 * x3 + x5)
  130. 0130specialize cf_convergent_matrix_state_prefix_transport (x2)
  131. 0131specialize cf_convergent_matrix_state_prefix_transport (x3)
  132. 0132apply cf_convergent_matrix_state_prefix_transport
  133. 0133exact hp
  134. 0134specialize succ_le_succ (S j)
  135. 0135specialize succ_le_succ (k)
  136. 0136apply succ_le_succ
  137. 0137exact heq_right
  138. 0138exact hs_witness_witness_witness_witness_witness_witness_witness_right_left
  139. 0139exact hs_witness_witness_witness_witness_witness_witness_witness_right_right