BA0043

cf_convergent_initial_matrix_exists

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

Every actual first quotient cell constructs the exact initial matrix [[q,1],[1,0]], including q=0.

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 q t. (s = S ((q + t) * S (q + t) + (t + t))) -> exists h e. (exists cfc_tail_initial_matrix. ((exists cfc_state_initial_matrixinitial. ((exists cfc_left_initial_matrixinitialcode cfc_right_initial_matrixinitialcode cfc_matrix_initial_matrixinitialcode. ((cfc_left_initial_matrixinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_initial_matrixinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_initial_matrixinitialcode = ((cfc_left_initial_matrixinitialcode) + (cfc_right_initial_matrixinitialcode)) * S ((cfc_left_initial_matrixinitialcode) + (cfc_right_initial_matrixinitialcode)) + ((cfc_right_initial_matrixinitialcode) + (cfc_right_initial_matrixinitialcode))) /\ ((cfc_state_initial_matrixinitial) = ((cfc_tail_initial_matrix) + (cfc_matrix_initial_matrixinitialcode)) * S ((cfc_tail_initial_matrix) + (cfc_matrix_initial_matrixinitialcode)) + ((cfc_matrix_initial_matrixinitialcode) + (cfc_matrix_initial_matrixinitialcode))))))) /\ (((exists ff_h_initial_matrixinitialentry. ff_h_initial_matrixinitialentry + S (cfc_state_initial_matrixinitial) = S ((S (0)) * e)) /\ exists ff_q_initial_matrixinitialentry. h = ff_q_initial_matrixinitialentry * S ((S (0)) * e) + (cfc_state_initial_matrixinitial))))) /\ ((exists cfc_state_initial_matrixterminal. ((exists cfc_left_initial_matrixterminalcode cfc_right_initial_matrixterminalcode cfc_matrix_initial_matrixterminalcode. ((cfc_left_initial_matrixterminalcode = ((q) + (1)) * S ((q) + (1)) + ((1) + (1))) /\ ((cfc_right_initial_matrixterminalcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_matrix_initial_matrixterminalcode = ((cfc_left_initial_matrixterminalcode) + (cfc_right_initial_matrixterminalcode)) * S ((cfc_left_initial_matrixterminalcode) + (cfc_right_initial_matrixterminalcode)) + ((cfc_right_initial_matrixterminalcode) + (cfc_right_initial_matrixterminalcode))) /\ ((cfc_state_initial_matrixterminal) = ((s) + (cfc_matrix_initial_matrixterminalcode)) * S ((s) + (cfc_matrix_initial_matrixterminalcode)) + ((cfc_matrix_initial_matrixterminalcode) + (cfc_matrix_initial_matrixterminalcode))))))) /\ (((exists ff_h_initial_matrixterminalentry. ff_h_initial_matrixterminalentry + S (cfc_state_initial_matrixterminal) = S ((S (1)) * e)) /\ exists ff_q_initial_matrixterminalentry. h = ff_q_initial_matrixterminalentry * S ((S (1)) * e) + (cfc_state_initial_matrixterminal))))) /\ (forall cfc_index_initial_matrix. (exists cfba_gap_initial_matrixbound. cfba_gap_initial_matrixbound + S (cfc_index_initial_matrix) = (1)) -> exists cfc_old_initial_matrix cfc_a_initial_matrix cfc_b_initial_matrix cfc_c_initial_matrix cfc_d_initial_matrix cfc_new_initial_matrix cfc_quotient_initial_matrix. ((exists cfc_state_initial_matrixprevious. ((exists cfc_left_initial_matrixpreviouscode cfc_right_initial_matrixpreviouscode cfc_matrix_initial_matrixpreviouscode. ((cfc_left_initial_matrixpreviouscode = ((cfc_a_initial_matrix) + (cfc_b_initial_matrix)) * S ((cfc_a_initial_matrix) + (cfc_b_initial_matrix)) + ((cfc_b_initial_matrix) + (cfc_b_initial_matrix))) /\ ((cfc_right_initial_matrixpreviouscode = ((cfc_c_initial_matrix) + (cfc_d_initial_matrix)) * S ((cfc_c_initial_matrix) + (cfc_d_initial_matrix)) + ((cfc_d_initial_matrix) + (cfc_d_initial_matrix))) /\ ((cfc_matrix_initial_matrixpreviouscode = ((cfc_left_initial_matrixpreviouscode) + (cfc_right_initial_matrixpreviouscode)) * S ((cfc_left_initial_matrixpreviouscode) + (cfc_right_initial_matrixpreviouscode)) + ((cfc_right_initial_matrixpreviouscode) + (cfc_right_initial_matrixpreviouscode))) /\ ((cfc_state_initial_matrixprevious) = ((cfc_old_initial_matrix) + (cfc_matrix_initial_matrixpreviouscode)) * S ((cfc_old_initial_matrix) + (cfc_matrix_initial_matrixpreviouscode)) + ((cfc_matrix_initial_matrixpreviouscode) + (cfc_matrix_initial_matrixpreviouscode))))))) /\ (((exists ff_h_initial_matrixpreviousentry. ff_h_initial_matrixpreviousentry + S (cfc_state_initial_matrixprevious) = S ((S (cfc_index_initial_matrix)) * e)) /\ exists ff_q_initial_matrixpreviousentry. h = ff_q_initial_matrixpreviousentry * S ((S (cfc_index_initial_matrix)) * e) + (cfc_state_initial_matrixprevious))))) /\ ((exists cfc_state_initial_matrixfollowing. ((exists cfc_left_initial_matrixfollowingcode cfc_right_initial_matrixfollowingcode cfc_matrix_initial_matrixfollowingcode. ((cfc_left_initial_matrixfollowingcode = (((cfc_quotient_initial_matrix * cfc_a_initial_matrix + cfc_c_initial_matrix)) + ((cfc_quotient_initial_matrix * cfc_b_initial_matrix + cfc_d_initial_matrix))) * S (((cfc_quotient_initial_matrix * cfc_a_initial_matrix + cfc_c_initial_matrix)) + ((cfc_quotient_initial_matrix * cfc_b_initial_matrix + cfc_d_initial_matrix))) + (((cfc_quotient_initial_matrix * cfc_b_initial_matrix + cfc_d_initial_matrix)) + ((cfc_quotient_initial_matrix * cfc_b_initial_matrix + cfc_d_initial_matrix)))) /\ ((cfc_right_initial_matrixfollowingcode = ((cfc_a_initial_matrix) + (cfc_b_initial_matrix)) * S ((cfc_a_initial_matrix) + (cfc_b_initial_matrix)) + ((cfc_b_initial_matrix) + (cfc_b_initial_matrix))) /\ ((cfc_matrix_initial_matrixfollowingcode = ((cfc_left_initial_matrixfollowingcode) + (cfc_right_initial_matrixfollowingcode)) * S ((cfc_left_initial_matrixfollowingcode) + (cfc_right_initial_matrixfollowingcode)) + ((cfc_right_initial_matrixfollowingcode) + (cfc_right_initial_matrixfollowingcode))) /\ ((cfc_state_initial_matrixfollowing) = ((cfc_new_initial_matrix) + (cfc_matrix_initial_matrixfollowingcode)) * S ((cfc_new_initial_matrix) + (cfc_matrix_initial_matrixfollowingcode)) + ((cfc_matrix_initial_matrixfollowingcode) + (cfc_matrix_initial_matrixfollowingcode))))))) /\ (((exists ff_h_initial_matrixfollowingentry. ff_h_initial_matrixfollowingentry + S (cfc_state_initial_matrixfollowing) = S ((S (S cfc_index_initial_matrix)) * e)) /\ exists ff_q_initial_matrixfollowingentry. h = ff_q_initial_matrixfollowingentry * S ((S (S cfc_index_initial_matrix)) * e) + (cfc_state_initial_matrixfollowing))))) /\ (cfc_new_initial_matrix = S ((cfc_quotient_initial_matrix + cfc_old_initial_matrix) * S (cfc_quotient_initial_matrix + cfc_old_initial_matrix) + (cfc_old_initial_matrix + cfc_old_initial_matrix)))))))))

Constructive proof overview

Generated structural guide

Every actual first quotient cell constructs the exact initial matrix [[q,1],[1,0]], including q=0.

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

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

Proof neighborhood

Direct dependencies

BA003A cf_convergent_matrix_empty_exists BA003C cf_convergent_matrix_prepend_exists BA0037 cf_convergent_matrix_entry_transport zero_add Stable theorem; checked-use authorized

Direct dependents

BA0044 continued_fraction_first_cell_is_initial_convergent 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

45 script commands · 11 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 (3)
cf convergent matrix empty existscf convergent matrix prepend existscf convergent matrix entry 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–4

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

  1. L1
    intro s
  2. L2
    intro q
  3. L3
    intro t
  4. L4
    intro hc
02Establish hzL5–7

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

  1. L5
    have hz : ∃ h. ∃ e. ConvergentMatrixTrace(t,h,e,0,1,0,0,1)Definitions: ConvergentMatrixTrace
  2. L6
    specialize cf_convergent_matrix_empty_exists (t)
  3. L7
    apply cf_convergent_matrix_empty_exists
03Separate the logical casesL8–9

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

  1. L8
    cases hz
  2. L9
    cases hz_witness
04Establish hnL10–19

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

  1. L10
    have hn : ∃ h. ∃ e. ConvergentMatrixTrace(s,h,e,1,q · 1 + 0,q · 0 + 1,1,0)Definitions: ConvergentMatrixTrace
  2. L11
    specialize cf_convergent_matrix_prepend_exists (t)
  3. L12
    specialize cf_convergent_matrix_prepend_exists (x)
  4. L13
    specialize cf_convergent_matrix_prepend_exists (x1)
  5. L14
    specialize cf_convergent_matrix_prepend_exists (0)
  6. L15
    specialize cf_convergent_matrix_prepend_exists (1)
  7. L16
    specialize cf_convergent_matrix_prepend_exists (0)
  8. L17
    specialize cf_convergent_matrix_prepend_exists (0)
  9. L18
    specialize cf_convergent_matrix_prepend_exists (1)
  10. L19
    specialize cf_convergent_matrix_prepend_exists (q)
05Use earlier factsL20–23

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

  1. L20
    specialize cf_convergent_matrix_prepend_exists (s)
  2. L21
    apply cf_convergent_matrix_prepend_exists
  3. L22
    exact hz_witness_witness
  4. L23
    exact hc
06Separate the logical casesL24–25

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

  1. L24
    cases hn
  2. L25
    cases hn_witness
07Construct an explicit witnessL26–27

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

  1. L26
    exists x2
  2. L27
    exists x3
08Use earlier factsL28–37

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

  1. L28
    specialize cf_convergent_matrix_entry_transport (s)
  2. L29
    specialize cf_convergent_matrix_entry_transport (x2)
  3. L30
    specialize cf_convergent_matrix_entry_transport (x3)
  4. L31
    specialize cf_convergent_matrix_entry_transport (1)
  5. L32
    specialize cf_convergent_matrix_entry_transport (q)
  6. L33
    specialize cf_convergent_matrix_entry_transport (1)
  7. L34
    specialize cf_convergent_matrix_entry_transport (1)
  8. L35
    specialize cf_convergent_matrix_entry_transport (0)
  9. L36
    specialize cf_convergent_matrix_entry_transport ((q * 1 + 0))
  10. L37
    specialize cf_convergent_matrix_entry_transport ((q * 0 + 1))
09Use earlier factsL38–40

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

  1. L38
    specialize cf_convergent_matrix_entry_transport (1)
  2. L39
    specialize cf_convergent_matrix_entry_transport (0)
  3. L40
    apply cf_convergent_matrix_entry_transport
10Calculate and transport equalitiesL41–44

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

  1. L41
    simp [zero_add]
  2. L42
    simp
  3. L43
    refl
  4. L44
    refl
11Use earlier factsL45–45

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

  1. L45
    exact hn_witness_witness

Library-wide reading audit

Original exact command ledger · 45 lines
  1. 0001intro s
  2. 0002intro q
  3. 0003intro t
  4. 0004intro hc
  5. 0005have hz : exists h e. exists cfc_tail_initial_empty. ((exists cfc_state_initial_emptyinitial. ((exists cfc_left_initial_emptyinitialcode cfc_right_initial_emptyinitialcode cfc_matrix_initial_emptyinitialcode. ((cfc_left_initial_emptyinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_initial_emptyinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_initial_emptyinitialcode = ((cfc_left_initial_emptyinitialcode) + (cfc_right_initial_emptyinitialcode)) * S ((cfc_left_initial_emptyinitialcode) + (cfc_right_initial_emptyinitialcode)) + ((cfc_right_initial_emptyinitialcode) + (cfc_right_initial_emptyinitialcode))) /\ ((cfc_state_initial_emptyinitial) = ((cfc_tail_initial_empty) + (cfc_matrix_initial_emptyinitialcode)) * S ((cfc_tail_initial_empty) + (cfc_matrix_initial_emptyinitialcode)) + ((cfc_matrix_initial_emptyinitialcode) + (cfc_matrix_initial_emptyinitialcode))))))) /\ (((exists ff_h_initial_emptyinitialentry. ff_h_initial_emptyinitialentry + S (cfc_state_initial_emptyinitial) = S ((S (0)) * e)) /\ exists ff_q_initial_emptyinitialentry. h = ff_q_initial_emptyinitialentry * S ((S (0)) * e) + (cfc_state_initial_emptyinitial))))) /\ ((exists cfc_state_initial_emptyterminal. ((exists cfc_left_initial_emptyterminalcode cfc_right_initial_emptyterminalcode cfc_matrix_initial_emptyterminalcode. ((cfc_left_initial_emptyterminalcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_initial_emptyterminalcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_initial_emptyterminalcode = ((cfc_left_initial_emptyterminalcode) + (cfc_right_initial_emptyterminalcode)) * S ((cfc_left_initial_emptyterminalcode) + (cfc_right_initial_emptyterminalcode)) + ((cfc_right_initial_emptyterminalcode) + (cfc_right_initial_emptyterminalcode))) /\ ((cfc_state_initial_emptyterminal) = ((t) + (cfc_matrix_initial_emptyterminalcode)) * S ((t) + (cfc_matrix_initial_emptyterminalcode)) + ((cfc_matrix_initial_emptyterminalcode) + (cfc_matrix_initial_emptyterminalcode))))))) /\ (((exists ff_h_initial_emptyterminalentry. ff_h_initial_emptyterminalentry + S (cfc_state_initial_emptyterminal) = S ((S (0)) * e)) /\ exists ff_q_initial_emptyterminalentry. h = ff_q_initial_emptyterminalentry * S ((S (0)) * e) + (cfc_state_initial_emptyterminal))))) /\ (forall cfc_index_initial_empty. (exists cfba_gap_initial_emptybound. cfba_gap_initial_emptybound + S (cfc_index_initial_empty) = (0)) -> exists cfc_old_initial_empty cfc_a_initial_empty cfc_b_initial_empty cfc_c_initial_empty cfc_d_initial_empty cfc_new_initial_empty cfc_quotient_initial_empty. ((exists cfc_state_initial_emptyprevious. ((exists cfc_left_initial_emptypreviouscode cfc_right_initial_emptypreviouscode cfc_matrix_initial_emptypreviouscode. ((cfc_left_initial_emptypreviouscode = ((cfc_a_initial_empty) + (cfc_b_initial_empty)) * S ((cfc_a_initial_empty) + (cfc_b_initial_empty)) + ((cfc_b_initial_empty) + (cfc_b_initial_empty))) /\ ((cfc_right_initial_emptypreviouscode = ((cfc_c_initial_empty) + (cfc_d_initial_empty)) * S ((cfc_c_initial_empty) + (cfc_d_initial_empty)) + ((cfc_d_initial_empty) + (cfc_d_initial_empty))) /\ ((cfc_matrix_initial_emptypreviouscode = ((cfc_left_initial_emptypreviouscode) + (cfc_right_initial_emptypreviouscode)) * S ((cfc_left_initial_emptypreviouscode) + (cfc_right_initial_emptypreviouscode)) + ((cfc_right_initial_emptypreviouscode) + (cfc_right_initial_emptypreviouscode))) /\ ((cfc_state_initial_emptyprevious) = ((cfc_old_initial_empty) + (cfc_matrix_initial_emptypreviouscode)) * S ((cfc_old_initial_empty) + (cfc_matrix_initial_emptypreviouscode)) + ((cfc_matrix_initial_emptypreviouscode) + (cfc_matrix_initial_emptypreviouscode))))))) /\ (((exists ff_h_initial_emptypreviousentry. ff_h_initial_emptypreviousentry + S (cfc_state_initial_emptyprevious) = S ((S (cfc_index_initial_empty)) * e)) /\ exists ff_q_initial_emptypreviousentry. h = ff_q_initial_emptypreviousentry * S ((S (cfc_index_initial_empty)) * e) + (cfc_state_initial_emptyprevious))))) /\ ((exists cfc_state_initial_emptyfollowing. ((exists cfc_left_initial_emptyfollowingcode cfc_right_initial_emptyfollowingcode cfc_matrix_initial_emptyfollowingcode. ((cfc_left_initial_emptyfollowingcode = (((cfc_quotient_initial_empty * cfc_a_initial_empty + cfc_c_initial_empty)) + ((cfc_quotient_initial_empty * cfc_b_initial_empty + cfc_d_initial_empty))) * S (((cfc_quotient_initial_empty * cfc_a_initial_empty + cfc_c_initial_empty)) + ((cfc_quotient_initial_empty * cfc_b_initial_empty + cfc_d_initial_empty))) + (((cfc_quotient_initial_empty * cfc_b_initial_empty + cfc_d_initial_empty)) + ((cfc_quotient_initial_empty * cfc_b_initial_empty + cfc_d_initial_empty)))) /\ ((cfc_right_initial_emptyfollowingcode = ((cfc_a_initial_empty) + (cfc_b_initial_empty)) * S ((cfc_a_initial_empty) + (cfc_b_initial_empty)) + ((cfc_b_initial_empty) + (cfc_b_initial_empty))) /\ ((cfc_matrix_initial_emptyfollowingcode = ((cfc_left_initial_emptyfollowingcode) + (cfc_right_initial_emptyfollowingcode)) * S ((cfc_left_initial_emptyfollowingcode) + (cfc_right_initial_emptyfollowingcode)) + ((cfc_right_initial_emptyfollowingcode) + (cfc_right_initial_emptyfollowingcode))) /\ ((cfc_state_initial_emptyfollowing) = ((cfc_new_initial_empty) + (cfc_matrix_initial_emptyfollowingcode)) * S ((cfc_new_initial_empty) + (cfc_matrix_initial_emptyfollowingcode)) + ((cfc_matrix_initial_emptyfollowingcode) + (cfc_matrix_initial_emptyfollowingcode))))))) /\ (((exists ff_h_initial_emptyfollowingentry. ff_h_initial_emptyfollowingentry + S (cfc_state_initial_emptyfollowing) = S ((S (S cfc_index_initial_empty)) * e)) /\ exists ff_q_initial_emptyfollowingentry. h = ff_q_initial_emptyfollowingentry * S ((S (S cfc_index_initial_empty)) * e) + (cfc_state_initial_emptyfollowing))))) /\ (cfc_new_initial_empty = S ((cfc_quotient_initial_empty + cfc_old_initial_empty) * S (cfc_quotient_initial_empty + cfc_old_initial_empty) + (cfc_old_initial_empty + cfc_old_initial_empty))))))))
  6. 0006specialize cf_convergent_matrix_empty_exists (t)
  7. 0007apply cf_convergent_matrix_empty_exists
  8. 0008cases hz
  9. 0009cases hz_witness
  10. 0010have hn : exists h e. exists cfc_tail_initial_prepend. ((exists cfc_state_initial_prependinitial. ((exists cfc_left_initial_prependinitialcode cfc_right_initial_prependinitialcode cfc_matrix_initial_prependinitialcode. ((cfc_left_initial_prependinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_initial_prependinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_initial_prependinitialcode = ((cfc_left_initial_prependinitialcode) + (cfc_right_initial_prependinitialcode)) * S ((cfc_left_initial_prependinitialcode) + (cfc_right_initial_prependinitialcode)) + ((cfc_right_initial_prependinitialcode) + (cfc_right_initial_prependinitialcode))) /\ ((cfc_state_initial_prependinitial) = ((cfc_tail_initial_prepend) + (cfc_matrix_initial_prependinitialcode)) * S ((cfc_tail_initial_prepend) + (cfc_matrix_initial_prependinitialcode)) + ((cfc_matrix_initial_prependinitialcode) + (cfc_matrix_initial_prependinitialcode))))))) /\ (((exists ff_h_initial_prependinitialentry. ff_h_initial_prependinitialentry + S (cfc_state_initial_prependinitial) = S ((S (0)) * e)) /\ exists ff_q_initial_prependinitialentry. h = ff_q_initial_prependinitialentry * S ((S (0)) * e) + (cfc_state_initial_prependinitial))))) /\ ((exists cfc_state_initial_prependterminal. ((exists cfc_left_initial_prependterminalcode cfc_right_initial_prependterminalcode cfc_matrix_initial_prependterminalcode. ((cfc_left_initial_prependterminalcode = (((q * 1 + 0)) + ((q * 0 + 1))) * S (((q * 1 + 0)) + ((q * 0 + 1))) + (((q * 0 + 1)) + ((q * 0 + 1)))) /\ ((cfc_right_initial_prependterminalcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_matrix_initial_prependterminalcode = ((cfc_left_initial_prependterminalcode) + (cfc_right_initial_prependterminalcode)) * S ((cfc_left_initial_prependterminalcode) + (cfc_right_initial_prependterminalcode)) + ((cfc_right_initial_prependterminalcode) + (cfc_right_initial_prependterminalcode))) /\ ((cfc_state_initial_prependterminal) = ((s) + (cfc_matrix_initial_prependterminalcode)) * S ((s) + (cfc_matrix_initial_prependterminalcode)) + ((cfc_matrix_initial_prependterminalcode) + (cfc_matrix_initial_prependterminalcode))))))) /\ (((exists ff_h_initial_prependterminalentry. ff_h_initial_prependterminalentry + S (cfc_state_initial_prependterminal) = S ((S (1)) * e)) /\ exists ff_q_initial_prependterminalentry. h = ff_q_initial_prependterminalentry * S ((S (1)) * e) + (cfc_state_initial_prependterminal))))) /\ (forall cfc_index_initial_prepend. (exists cfba_gap_initial_prependbound. cfba_gap_initial_prependbound + S (cfc_index_initial_prepend) = (1)) -> exists cfc_old_initial_prepend cfc_a_initial_prepend cfc_b_initial_prepend cfc_c_initial_prepend cfc_d_initial_prepend cfc_new_initial_prepend cfc_quotient_initial_prepend. ((exists cfc_state_initial_prependprevious. ((exists cfc_left_initial_prependpreviouscode cfc_right_initial_prependpreviouscode cfc_matrix_initial_prependpreviouscode. ((cfc_left_initial_prependpreviouscode = ((cfc_a_initial_prepend) + (cfc_b_initial_prepend)) * S ((cfc_a_initial_prepend) + (cfc_b_initial_prepend)) + ((cfc_b_initial_prepend) + (cfc_b_initial_prepend))) /\ ((cfc_right_initial_prependpreviouscode = ((cfc_c_initial_prepend) + (cfc_d_initial_prepend)) * S ((cfc_c_initial_prepend) + (cfc_d_initial_prepend)) + ((cfc_d_initial_prepend) + (cfc_d_initial_prepend))) /\ ((cfc_matrix_initial_prependpreviouscode = ((cfc_left_initial_prependpreviouscode) + (cfc_right_initial_prependpreviouscode)) * S ((cfc_left_initial_prependpreviouscode) + (cfc_right_initial_prependpreviouscode)) + ((cfc_right_initial_prependpreviouscode) + (cfc_right_initial_prependpreviouscode))) /\ ((cfc_state_initial_prependprevious) = ((cfc_old_initial_prepend) + (cfc_matrix_initial_prependpreviouscode)) * S ((cfc_old_initial_prepend) + (cfc_matrix_initial_prependpreviouscode)) + ((cfc_matrix_initial_prependpreviouscode) + (cfc_matrix_initial_prependpreviouscode))))))) /\ (((exists ff_h_initial_prependpreviousentry. ff_h_initial_prependpreviousentry + S (cfc_state_initial_prependprevious) = S ((S (cfc_index_initial_prepend)) * e)) /\ exists ff_q_initial_prependpreviousentry. h = ff_q_initial_prependpreviousentry * S ((S (cfc_index_initial_prepend)) * e) + (cfc_state_initial_prependprevious))))) /\ ((exists cfc_state_initial_prependfollowing. ((exists cfc_left_initial_prependfollowingcode cfc_right_initial_prependfollowingcode cfc_matrix_initial_prependfollowingcode. ((cfc_left_initial_prependfollowingcode = (((cfc_quotient_initial_prepend * cfc_a_initial_prepend + cfc_c_initial_prepend)) + ((cfc_quotient_initial_prepend * cfc_b_initial_prepend + cfc_d_initial_prepend))) * S (((cfc_quotient_initial_prepend * cfc_a_initial_prepend + cfc_c_initial_prepend)) + ((cfc_quotient_initial_prepend * cfc_b_initial_prepend + cfc_d_initial_prepend))) + (((cfc_quotient_initial_prepend * cfc_b_initial_prepend + cfc_d_initial_prepend)) + ((cfc_quotient_initial_prepend * cfc_b_initial_prepend + cfc_d_initial_prepend)))) /\ ((cfc_right_initial_prependfollowingcode = ((cfc_a_initial_prepend) + (cfc_b_initial_prepend)) * S ((cfc_a_initial_prepend) + (cfc_b_initial_prepend)) + ((cfc_b_initial_prepend) + (cfc_b_initial_prepend))) /\ ((cfc_matrix_initial_prependfollowingcode = ((cfc_left_initial_prependfollowingcode) + (cfc_right_initial_prependfollowingcode)) * S ((cfc_left_initial_prependfollowingcode) + (cfc_right_initial_prependfollowingcode)) + ((cfc_right_initial_prependfollowingcode) + (cfc_right_initial_prependfollowingcode))) /\ ((cfc_state_initial_prependfollowing) = ((cfc_new_initial_prepend) + (cfc_matrix_initial_prependfollowingcode)) * S ((cfc_new_initial_prepend) + (cfc_matrix_initial_prependfollowingcode)) + ((cfc_matrix_initial_prependfollowingcode) + (cfc_matrix_initial_prependfollowingcode))))))) /\ (((exists ff_h_initial_prependfollowingentry. ff_h_initial_prependfollowingentry + S (cfc_state_initial_prependfollowing) = S ((S (S cfc_index_initial_prepend)) * e)) /\ exists ff_q_initial_prependfollowingentry. h = ff_q_initial_prependfollowingentry * S ((S (S cfc_index_initial_prepend)) * e) + (cfc_state_initial_prependfollowing))))) /\ (cfc_new_initial_prepend = S ((cfc_quotient_initial_prepend + cfc_old_initial_prepend) * S (cfc_quotient_initial_prepend + cfc_old_initial_prepend) + (cfc_old_initial_prepend + cfc_old_initial_prepend))))))))
  11. 0011specialize cf_convergent_matrix_prepend_exists (t)
  12. 0012specialize cf_convergent_matrix_prepend_exists (x)
  13. 0013specialize cf_convergent_matrix_prepend_exists (x1)
  14. 0014specialize cf_convergent_matrix_prepend_exists (0)
  15. 0015specialize cf_convergent_matrix_prepend_exists (1)
  16. 0016specialize cf_convergent_matrix_prepend_exists (0)
  17. 0017specialize cf_convergent_matrix_prepend_exists (0)
  18. 0018specialize cf_convergent_matrix_prepend_exists (1)
  19. 0019specialize cf_convergent_matrix_prepend_exists (q)
  20. 0020specialize cf_convergent_matrix_prepend_exists (s)
  21. 0021apply cf_convergent_matrix_prepend_exists
  22. 0022exact hz_witness_witness
  23. 0023exact hc
  24. 0024cases hn
  25. 0025cases hn_witness
  26. 0026exists x2
  27. 0027exists x3
  28. 0028specialize cf_convergent_matrix_entry_transport (s)
  29. 0029specialize cf_convergent_matrix_entry_transport (x2)
  30. 0030specialize cf_convergent_matrix_entry_transport (x3)
  31. 0031specialize cf_convergent_matrix_entry_transport (1)
  32. 0032specialize cf_convergent_matrix_entry_transport (q)
  33. 0033specialize cf_convergent_matrix_entry_transport (1)
  34. 0034specialize cf_convergent_matrix_entry_transport (1)
  35. 0035specialize cf_convergent_matrix_entry_transport (0)
  36. 0036specialize cf_convergent_matrix_entry_transport ((q * 1 + 0))
  37. 0037specialize cf_convergent_matrix_entry_transport ((q * 0 + 1))
  38. 0038specialize cf_convergent_matrix_entry_transport (1)
  39. 0039specialize cf_convergent_matrix_entry_transport (0)
  40. 0040apply cf_convergent_matrix_entry_transport
  41. 0041simp [zero_add]
  42. 0042simp
  43. 0043refl
  44. 0044refl
  45. 0045exact hn_witness_witness