BA004C

continued_fraction_convergent_functional

An actual indexed convergent has a unique natural numerator and positive denominator, independently of every auxiliary matrix-history certificate.

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

∀ s. ∀ i. ∀ u. ∀ v. ∀ p. ∀ q. Convergent(s,i,u,v) → Convergent(s,i,p,q) → u = p ∧ v = q

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

Convergent(s,i,u,v) · 2

Actual proof prerequisites

cf_convergent_matrix_prefix_functional
Original expanded first-order statement 
forall s i u v p q. (exists cfc_previous_numerator_functional_convergent_first cfc_previous_denominator_functional_convergent_first cfc_code_functional_convergent_first cfc_scale_functional_convergent_first. ((~(v = 0)) /\ (exists cfc_tail_functional_convergent_firstcomputation. ((exists cfc_state_functional_convergent_firstcomputationinitial. ((exists cfc_left_functional_convergent_firstcomputationinitialcode cfc_right_functional_convergent_firstcomputationinitialcode cfc_matrix_functional_convergent_firstcomputationinitialcode. ((cfc_left_functional_convergent_firstcomputationinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_functional_convergent_firstcomputationinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_functional_convergent_firstcomputationinitialcode = ((cfc_left_functional_convergent_firstcomputationinitialcode) + (cfc_right_functional_convergent_firstcomputationinitialcode)) * S ((cfc_left_functional_convergent_firstcomputationinitialcode) + (cfc_right_functional_convergent_firstcomputationinitialcode)) + ((cfc_right_functional_convergent_firstcomputationinitialcode) + (cfc_right_functional_convergent_firstcomputationinitialcode))) /\ ((cfc_state_functional_convergent_firstcomputationinitial) = ((cfc_tail_functional_convergent_firstcomputation) + (cfc_matrix_functional_convergent_firstcomputationinitialcode)) * S ((cfc_tail_functional_convergent_firstcomputation) + (cfc_matrix_functional_convergent_firstcomputationinitialcode)) + ((cfc_matrix_functional_convergent_firstcomputationinitialcode) + (cfc_matrix_functional_convergent_firstcomputationinitialcode))))))) /\ (((exists ff_h_functional_convergent_firstcomputationinitialentry. ff_h_functional_convergent_firstcomputationinitialentry + S (cfc_state_functional_convergent_firstcomputationinitial) = S ((S (0)) * cfc_scale_functional_convergent_first)) /\ exists ff_q_functional_convergent_firstcomputationinitialentry. cfc_code_functional_convergent_first = ff_q_functional_convergent_firstcomputationinitialentry * S ((S (0)) * cfc_scale_functional_convergent_first) + (cfc_state_functional_convergent_firstcomputationinitial))))) /\ ((exists cfc_state_functional_convergent_firstcomputationterminal. ((exists cfc_left_functional_convergent_firstcomputationterminalcode cfc_right_functional_convergent_firstcomputationterminalcode cfc_matrix_functional_convergent_firstcomputationterminalcode. ((cfc_left_functional_convergent_firstcomputationterminalcode = ((u) + (cfc_previous_numerator_functional_convergent_first)) * S ((u) + (cfc_previous_numerator_functional_convergent_first)) + ((cfc_previous_numerator_functional_convergent_first) + (cfc_previous_numerator_functional_convergent_first))) /\ ((cfc_right_functional_convergent_firstcomputationterminalcode = ((v) + (cfc_previous_denominator_functional_convergent_first)) * S ((v) + (cfc_previous_denominator_functional_convergent_first)) + ((cfc_previous_denominator_functional_convergent_first) + (cfc_previous_denominator_functional_convergent_first))) /\ ((cfc_matrix_functional_convergent_firstcomputationterminalcode = ((cfc_left_functional_convergent_firstcomputationterminalcode) + (cfc_right_functional_convergent_firstcomputationterminalcode)) * S ((cfc_left_functional_convergent_firstcomputationterminalcode) + (cfc_right_functional_convergent_firstcomputationterminalcode)) + ((cfc_right_functional_convergent_firstcomputationterminalcode) + (cfc_right_functional_convergent_firstcomputationterminalcode))) /\ ((cfc_state_functional_convergent_firstcomputationterminal) = ((s) + (cfc_matrix_functional_convergent_firstcomputationterminalcode)) * S ((s) + (cfc_matrix_functional_convergent_firstcomputationterminalcode)) + ((cfc_matrix_functional_convergent_firstcomputationterminalcode) + (cfc_matrix_functional_convergent_firstcomputationterminalcode))))))) /\ (((exists ff_h_functional_convergent_firstcomputationterminalentry. ff_h_functional_convergent_firstcomputationterminalentry + S (cfc_state_functional_convergent_firstcomputationterminal) = S ((S (S (i))) * cfc_scale_functional_convergent_first)) /\ exists ff_q_functional_convergent_firstcomputationterminalentry. cfc_code_functional_convergent_first = ff_q_functional_convergent_firstcomputationterminalentry * S ((S (S (i))) * cfc_scale_functional_convergent_first) + (cfc_state_functional_convergent_firstcomputationterminal))))) /\ (forall cfc_index_functional_convergent_firstcomputation. (exists cfba_gap_functional_convergent_firstcomputationbound. cfba_gap_functional_convergent_firstcomputationbound + S (cfc_index_functional_convergent_firstcomputation) = (S (i))) -> exists cfc_old_functional_convergent_firstcomputation cfc_a_functional_convergent_firstcomputation cfc_b_functional_convergent_firstcomputation cfc_c_functional_convergent_firstcomputation cfc_d_functional_convergent_firstcomputation cfc_new_functional_convergent_firstcomputation cfc_quotient_functional_convergent_firstcomputation. ((exists cfc_state_functional_convergent_firstcomputationprevious. ((exists cfc_left_functional_convergent_firstcomputationpreviouscode cfc_right_functional_convergent_firstcomputationpreviouscode cfc_matrix_functional_convergent_firstcomputationpreviouscode. ((cfc_left_functional_convergent_firstcomputationpreviouscode = ((cfc_a_functional_convergent_firstcomputation) + (cfc_b_functional_convergent_firstcomputation)) * S ((cfc_a_functional_convergent_firstcomputation) + (cfc_b_functional_convergent_firstcomputation)) + ((cfc_b_functional_convergent_firstcomputation) + (cfc_b_functional_convergent_firstcomputation))) /\ ((cfc_right_functional_convergent_firstcomputationpreviouscode = ((cfc_c_functional_convergent_firstcomputation) + (cfc_d_functional_convergent_firstcomputation)) * S ((cfc_c_functional_convergent_firstcomputation) + (cfc_d_functional_convergent_firstcomputation)) + ((cfc_d_functional_convergent_firstcomputation) + (cfc_d_functional_convergent_firstcomputation))) /\ ((cfc_matrix_functional_convergent_firstcomputationpreviouscode = ((cfc_left_functional_convergent_firstcomputationpreviouscode) + (cfc_right_functional_convergent_firstcomputationpreviouscode)) * S ((cfc_left_functional_convergent_firstcomputationpreviouscode) + (cfc_right_functional_convergent_firstcomputationpreviouscode)) + ((cfc_right_functional_convergent_firstcomputationpreviouscode) + (cfc_right_functional_convergent_firstcomputationpreviouscode))) /\ ((cfc_state_functional_convergent_firstcomputationprevious) = ((cfc_old_functional_convergent_firstcomputation) + (cfc_matrix_functional_convergent_firstcomputationpreviouscode)) * S ((cfc_old_functional_convergent_firstcomputation) + (cfc_matrix_functional_convergent_firstcomputationpreviouscode)) + ((cfc_matrix_functional_convergent_firstcomputationpreviouscode) + (cfc_matrix_functional_convergent_firstcomputationpreviouscode))))))) /\ (((exists ff_h_functional_convergent_firstcomputationpreviousentry. ff_h_functional_convergent_firstcomputationpreviousentry + S (cfc_state_functional_convergent_firstcomputationprevious) = S ((S (cfc_index_functional_convergent_firstcomputation)) * cfc_scale_functional_convergent_first)) /\ exists ff_q_functional_convergent_firstcomputationpreviousentry. cfc_code_functional_convergent_first = ff_q_functional_convergent_firstcomputationpreviousentry * S ((S (cfc_index_functional_convergent_firstcomputation)) * cfc_scale_functional_convergent_first) + (cfc_state_functional_convergent_firstcomputationprevious))))) /\ ((exists cfc_state_functional_convergent_firstcomputationfollowing. ((exists cfc_left_functional_convergent_firstcomputationfollowingcode cfc_right_functional_convergent_firstcomputationfollowingcode cfc_matrix_functional_convergent_firstcomputationfollowingcode. ((cfc_left_functional_convergent_firstcomputationfollowingcode = (((cfc_quotient_functional_convergent_firstcomputation * cfc_a_functional_convergent_firstcomputation + cfc_c_functional_convergent_firstcomputation)) + ((cfc_quotient_functional_convergent_firstcomputation * cfc_b_functional_convergent_firstcomputation + cfc_d_functional_convergent_firstcomputation))) * S (((cfc_quotient_functional_convergent_firstcomputation * cfc_a_functional_convergent_firstcomputation + cfc_c_functional_convergent_firstcomputation)) + ((cfc_quotient_functional_convergent_firstcomputation * cfc_b_functional_convergent_firstcomputation + cfc_d_functional_convergent_firstcomputation))) + (((cfc_quotient_functional_convergent_firstcomputation * cfc_b_functional_convergent_firstcomputation + cfc_d_functional_convergent_firstcomputation)) + ((cfc_quotient_functional_convergent_firstcomputation * cfc_b_functional_convergent_firstcomputation + cfc_d_functional_convergent_firstcomputation)))) /\ ((cfc_right_functional_convergent_firstcomputationfollowingcode = ((cfc_a_functional_convergent_firstcomputation) + (cfc_b_functional_convergent_firstcomputation)) * S ((cfc_a_functional_convergent_firstcomputation) + (cfc_b_functional_convergent_firstcomputation)) + ((cfc_b_functional_convergent_firstcomputation) + (cfc_b_functional_convergent_firstcomputation))) /\ ((cfc_matrix_functional_convergent_firstcomputationfollowingcode = ((cfc_left_functional_convergent_firstcomputationfollowingcode) + (cfc_right_functional_convergent_firstcomputationfollowingcode)) * S ((cfc_left_functional_convergent_firstcomputationfollowingcode) + (cfc_right_functional_convergent_firstcomputationfollowingcode)) + ((cfc_right_functional_convergent_firstcomputationfollowingcode) + (cfc_right_functional_convergent_firstcomputationfollowingcode))) /\ ((cfc_state_functional_convergent_firstcomputationfollowing) = ((cfc_new_functional_convergent_firstcomputation) + (cfc_matrix_functional_convergent_firstcomputationfollowingcode)) * S ((cfc_new_functional_convergent_firstcomputation) + (cfc_matrix_functional_convergent_firstcomputationfollowingcode)) + ((cfc_matrix_functional_convergent_firstcomputationfollowingcode) + (cfc_matrix_functional_convergent_firstcomputationfollowingcode))))))) /\ (((exists ff_h_functional_convergent_firstcomputationfollowingentry. ff_h_functional_convergent_firstcomputationfollowingentry + S (cfc_state_functional_convergent_firstcomputationfollowing) = S ((S (S cfc_index_functional_convergent_firstcomputation)) * cfc_scale_functional_convergent_first)) /\ exists ff_q_functional_convergent_firstcomputationfollowingentry. cfc_code_functional_convergent_first = ff_q_functional_convergent_firstcomputationfollowingentry * S ((S (S cfc_index_functional_convergent_firstcomputation)) * cfc_scale_functional_convergent_first) + (cfc_state_functional_convergent_firstcomputationfollowing))))) /\ (cfc_new_functional_convergent_firstcomputation = S ((cfc_quotient_functional_convergent_firstcomputation + cfc_old_functional_convergent_firstcomputation) * S (cfc_quotient_functional_convergent_firstcomputation + cfc_old_functional_convergent_firstcomputation) + (cfc_old_functional_convergent_firstcomputation + cfc_old_functional_convergent_firstcomputation))))))))))) -> (exists cfc_previous_numerator_functional_convergent_second cfc_previous_denominator_functional_convergent_second cfc_code_functional_convergent_second cfc_scale_functional_convergent_second. ((~(q = 0)) /\ (exists cfc_tail_functional_convergent_secondcomputation. ((exists cfc_state_functional_convergent_secondcomputationinitial. ((exists cfc_left_functional_convergent_secondcomputationinitialcode cfc_right_functional_convergent_secondcomputationinitialcode cfc_matrix_functional_convergent_secondcomputationinitialcode. ((cfc_left_functional_convergent_secondcomputationinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_functional_convergent_secondcomputationinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_functional_convergent_secondcomputationinitialcode = ((cfc_left_functional_convergent_secondcomputationinitialcode) + (cfc_right_functional_convergent_secondcomputationinitialcode)) * S ((cfc_left_functional_convergent_secondcomputationinitialcode) + (cfc_right_functional_convergent_secondcomputationinitialcode)) + ((cfc_right_functional_convergent_secondcomputationinitialcode) + (cfc_right_functional_convergent_secondcomputationinitialcode))) /\ ((cfc_state_functional_convergent_secondcomputationinitial) = ((cfc_tail_functional_convergent_secondcomputation) + (cfc_matrix_functional_convergent_secondcomputationinitialcode)) * S ((cfc_tail_functional_convergent_secondcomputation) + (cfc_matrix_functional_convergent_secondcomputationinitialcode)) + ((cfc_matrix_functional_convergent_secondcomputationinitialcode) + (cfc_matrix_functional_convergent_secondcomputationinitialcode))))))) /\ (((exists ff_h_functional_convergent_secondcomputationinitialentry. ff_h_functional_convergent_secondcomputationinitialentry + S (cfc_state_functional_convergent_secondcomputationinitial) = S ((S (0)) * cfc_scale_functional_convergent_second)) /\ exists ff_q_functional_convergent_secondcomputationinitialentry. cfc_code_functional_convergent_second = ff_q_functional_convergent_secondcomputationinitialentry * S ((S (0)) * cfc_scale_functional_convergent_second) + (cfc_state_functional_convergent_secondcomputationinitial))))) /\ ((exists cfc_state_functional_convergent_secondcomputationterminal. ((exists cfc_left_functional_convergent_secondcomputationterminalcode cfc_right_functional_convergent_secondcomputationterminalcode cfc_matrix_functional_convergent_secondcomputationterminalcode. ((cfc_left_functional_convergent_secondcomputationterminalcode = ((p) + (cfc_previous_numerator_functional_convergent_second)) * S ((p) + (cfc_previous_numerator_functional_convergent_second)) + ((cfc_previous_numerator_functional_convergent_second) + (cfc_previous_numerator_functional_convergent_second))) /\ ((cfc_right_functional_convergent_secondcomputationterminalcode = ((q) + (cfc_previous_denominator_functional_convergent_second)) * S ((q) + (cfc_previous_denominator_functional_convergent_second)) + ((cfc_previous_denominator_functional_convergent_second) + (cfc_previous_denominator_functional_convergent_second))) /\ ((cfc_matrix_functional_convergent_secondcomputationterminalcode = ((cfc_left_functional_convergent_secondcomputationterminalcode) + (cfc_right_functional_convergent_secondcomputationterminalcode)) * S ((cfc_left_functional_convergent_secondcomputationterminalcode) + (cfc_right_functional_convergent_secondcomputationterminalcode)) + ((cfc_right_functional_convergent_secondcomputationterminalcode) + (cfc_right_functional_convergent_secondcomputationterminalcode))) /\ ((cfc_state_functional_convergent_secondcomputationterminal) = ((s) + (cfc_matrix_functional_convergent_secondcomputationterminalcode)) * S ((s) + (cfc_matrix_functional_convergent_secondcomputationterminalcode)) + ((cfc_matrix_functional_convergent_secondcomputationterminalcode) + (cfc_matrix_functional_convergent_secondcomputationterminalcode))))))) /\ (((exists ff_h_functional_convergent_secondcomputationterminalentry. ff_h_functional_convergent_secondcomputationterminalentry + S (cfc_state_functional_convergent_secondcomputationterminal) = S ((S (S (i))) * cfc_scale_functional_convergent_second)) /\ exists ff_q_functional_convergent_secondcomputationterminalentry. cfc_code_functional_convergent_second = ff_q_functional_convergent_secondcomputationterminalentry * S ((S (S (i))) * cfc_scale_functional_convergent_second) + (cfc_state_functional_convergent_secondcomputationterminal))))) /\ (forall cfc_index_functional_convergent_secondcomputation. (exists cfba_gap_functional_convergent_secondcomputationbound. cfba_gap_functional_convergent_secondcomputationbound + S (cfc_index_functional_convergent_secondcomputation) = (S (i))) -> exists cfc_old_functional_convergent_secondcomputation cfc_a_functional_convergent_secondcomputation cfc_b_functional_convergent_secondcomputation cfc_c_functional_convergent_secondcomputation cfc_d_functional_convergent_secondcomputation cfc_new_functional_convergent_secondcomputation cfc_quotient_functional_convergent_secondcomputation. ((exists cfc_state_functional_convergent_secondcomputationprevious. ((exists cfc_left_functional_convergent_secondcomputationpreviouscode cfc_right_functional_convergent_secondcomputationpreviouscode cfc_matrix_functional_convergent_secondcomputationpreviouscode. ((cfc_left_functional_convergent_secondcomputationpreviouscode = ((cfc_a_functional_convergent_secondcomputation) + (cfc_b_functional_convergent_secondcomputation)) * S ((cfc_a_functional_convergent_secondcomputation) + (cfc_b_functional_convergent_secondcomputation)) + ((cfc_b_functional_convergent_secondcomputation) + (cfc_b_functional_convergent_secondcomputation))) /\ ((cfc_right_functional_convergent_secondcomputationpreviouscode = ((cfc_c_functional_convergent_secondcomputation) + (cfc_d_functional_convergent_secondcomputation)) * S ((cfc_c_functional_convergent_secondcomputation) + (cfc_d_functional_convergent_secondcomputation)) + ((cfc_d_functional_convergent_secondcomputation) + (cfc_d_functional_convergent_secondcomputation))) /\ ((cfc_matrix_functional_convergent_secondcomputationpreviouscode = ((cfc_left_functional_convergent_secondcomputationpreviouscode) + (cfc_right_functional_convergent_secondcomputationpreviouscode)) * S ((cfc_left_functional_convergent_secondcomputationpreviouscode) + (cfc_right_functional_convergent_secondcomputationpreviouscode)) + ((cfc_right_functional_convergent_secondcomputationpreviouscode) + (cfc_right_functional_convergent_secondcomputationpreviouscode))) /\ ((cfc_state_functional_convergent_secondcomputationprevious) = ((cfc_old_functional_convergent_secondcomputation) + (cfc_matrix_functional_convergent_secondcomputationpreviouscode)) * S ((cfc_old_functional_convergent_secondcomputation) + (cfc_matrix_functional_convergent_secondcomputationpreviouscode)) + ((cfc_matrix_functional_convergent_secondcomputationpreviouscode) + (cfc_matrix_functional_convergent_secondcomputationpreviouscode))))))) /\ (((exists ff_h_functional_convergent_secondcomputationpreviousentry. ff_h_functional_convergent_secondcomputationpreviousentry + S (cfc_state_functional_convergent_secondcomputationprevious) = S ((S (cfc_index_functional_convergent_secondcomputation)) * cfc_scale_functional_convergent_second)) /\ exists ff_q_functional_convergent_secondcomputationpreviousentry. cfc_code_functional_convergent_second = ff_q_functional_convergent_secondcomputationpreviousentry * S ((S (cfc_index_functional_convergent_secondcomputation)) * cfc_scale_functional_convergent_second) + (cfc_state_functional_convergent_secondcomputationprevious))))) /\ ((exists cfc_state_functional_convergent_secondcomputationfollowing. ((exists cfc_left_functional_convergent_secondcomputationfollowingcode cfc_right_functional_convergent_secondcomputationfollowingcode cfc_matrix_functional_convergent_secondcomputationfollowingcode. ((cfc_left_functional_convergent_secondcomputationfollowingcode = (((cfc_quotient_functional_convergent_secondcomputation * cfc_a_functional_convergent_secondcomputation + cfc_c_functional_convergent_secondcomputation)) + ((cfc_quotient_functional_convergent_secondcomputation * cfc_b_functional_convergent_secondcomputation + cfc_d_functional_convergent_secondcomputation))) * S (((cfc_quotient_functional_convergent_secondcomputation * cfc_a_functional_convergent_secondcomputation + cfc_c_functional_convergent_secondcomputation)) + ((cfc_quotient_functional_convergent_secondcomputation * cfc_b_functional_convergent_secondcomputation + cfc_d_functional_convergent_secondcomputation))) + (((cfc_quotient_functional_convergent_secondcomputation * cfc_b_functional_convergent_secondcomputation + cfc_d_functional_convergent_secondcomputation)) + ((cfc_quotient_functional_convergent_secondcomputation * cfc_b_functional_convergent_secondcomputation + cfc_d_functional_convergent_secondcomputation)))) /\ ((cfc_right_functional_convergent_secondcomputationfollowingcode = ((cfc_a_functional_convergent_secondcomputation) + (cfc_b_functional_convergent_secondcomputation)) * S ((cfc_a_functional_convergent_secondcomputation) + (cfc_b_functional_convergent_secondcomputation)) + ((cfc_b_functional_convergent_secondcomputation) + (cfc_b_functional_convergent_secondcomputation))) /\ ((cfc_matrix_functional_convergent_secondcomputationfollowingcode = ((cfc_left_functional_convergent_secondcomputationfollowingcode) + (cfc_right_functional_convergent_secondcomputationfollowingcode)) * S ((cfc_left_functional_convergent_secondcomputationfollowingcode) + (cfc_right_functional_convergent_secondcomputationfollowingcode)) + ((cfc_right_functional_convergent_secondcomputationfollowingcode) + (cfc_right_functional_convergent_secondcomputationfollowingcode))) /\ ((cfc_state_functional_convergent_secondcomputationfollowing) = ((cfc_new_functional_convergent_secondcomputation) + (cfc_matrix_functional_convergent_secondcomputationfollowingcode)) * S ((cfc_new_functional_convergent_secondcomputation) + (cfc_matrix_functional_convergent_secondcomputationfollowingcode)) + ((cfc_matrix_functional_convergent_secondcomputationfollowingcode) + (cfc_matrix_functional_convergent_secondcomputationfollowingcode))))))) /\ (((exists ff_h_functional_convergent_secondcomputationfollowingentry. ff_h_functional_convergent_secondcomputationfollowingentry + S (cfc_state_functional_convergent_secondcomputationfollowing) = S ((S (S cfc_index_functional_convergent_secondcomputation)) * cfc_scale_functional_convergent_second)) /\ exists ff_q_functional_convergent_secondcomputationfollowingentry. cfc_code_functional_convergent_second = ff_q_functional_convergent_secondcomputationfollowingentry * S ((S (S cfc_index_functional_convergent_secondcomputation)) * cfc_scale_functional_convergent_second) + (cfc_state_functional_convergent_secondcomputationfollowing))))) /\ (cfc_new_functional_convergent_secondcomputation = S ((cfc_quotient_functional_convergent_secondcomputation + cfc_old_functional_convergent_secondcomputation) * S (cfc_quotient_functional_convergent_secondcomputation + cfc_old_functional_convergent_secondcomputation) + (cfc_old_functional_convergent_secondcomputation + cfc_old_functional_convergent_secondcomputation))))))))))) -> u = p /\ v = q

Complete tactic proof in conservative notation

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

42 script commands · 6 reading checkpoints · 1 local claims

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

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 (1)
cf convergent matrix prefix functional
01Fix variables and assumptionsL1–8

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

  1. L1
    intro s
  2. L2
    intro i
  3. L3
    intro u
  4. L4
    intro v
  5. L5
    intro p
  6. L6
    intro q
  7. L7
    intro hc1
  8. L8
    intro hc2
02Separate the logical casesL9–18

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

  1. L9
    cases hc1
  2. L10
    cases hc1_witness
  3. L11
    cases hc1_witness_witness
  4. L12
    cases hc1_witness_witness_witness
  5. L13
    cases hc2
  6. L14
    cases hc2_witness
  7. L15
    cases hc2_witness_witness
  8. L16
    cases hc2_witness_witness_witness
  9. L17
    cases hc1_witness_witness_witness_witness
  10. L18
    cases hc2_witness_witness_witness_witness
03Establish heqL19–28

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

  1. L19
    have heq : ((u = p) /\ ((x = x4) /\ ((v = q) /\ (x1 = x5))))
  2. L20
    specialize cf_convergent_matrix_prefix_functional (S i)
  3. L21
    specialize cf_convergent_matrix_prefix_functional (s)
  4. L22
    specialize cf_convergent_matrix_prefix_functional (x2)
  5. L23
    specialize cf_convergent_matrix_prefix_functional (x3)
  6. L24
    specialize cf_convergent_matrix_prefix_functional (x6)
  7. L25
    specialize cf_convergent_matrix_prefix_functional (x7)
  8. L26
    specialize cf_convergent_matrix_prefix_functional (u)
  9. L27
    specialize cf_convergent_matrix_prefix_functional (x)
  10. L28
    specialize cf_convergent_matrix_prefix_functional (v)
04Use earlier factsL29–36

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

  1. L29
    specialize cf_convergent_matrix_prefix_functional (x1)
  2. L30
    specialize cf_convergent_matrix_prefix_functional (p)
  3. L31
    specialize cf_convergent_matrix_prefix_functional (x4)
  4. L32
    specialize cf_convergent_matrix_prefix_functional (q)
  5. L33
    specialize cf_convergent_matrix_prefix_functional (x5)
  6. L34
    apply cf_convergent_matrix_prefix_functional
  7. L35
    exact hc1_witness_witness_witness_witness_right
  8. L36
    exact hc2_witness_witness_witness_witness_right
05Separate the logical casesL37–40

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

  1. L37
    cases heq
  2. L38
    cases heq_right
  3. L39
    cases heq_right_right
  4. L40
    split
06Use earlier factsL41–42

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

  1. L41
    exact heq_left
  2. L42
    exact heq_right_right_left

Library-wide reading audit

Original defined command ledger · 42 lines
  1. 0001intro s
  2. 0002intro i
  3. 0003intro u
  4. 0004intro v
  5. 0005intro p
  6. 0006intro q
  7. 0007intro hc1
  8. 0008intro hc2
  9. 0009cases hc1
  10. 0010cases hc1_witness
  11. 0011cases hc1_witness_witness
  12. 0012cases hc1_witness_witness_witness
  13. 0013cases hc2
  14. 0014cases hc2_witness
  15. 0015cases hc2_witness_witness
  16. 0016cases hc2_witness_witness_witness
  17. 0017cases hc1_witness_witness_witness_witness
  18. 0018cases hc2_witness_witness_witness_witness
  19. 0019have heq : ((u = p) /\ ((x = x4) /\ ((v = q) /\ (x1 = x5))))
  20. 0020specialize cf_convergent_matrix_prefix_functional (S i)
  21. 0021specialize cf_convergent_matrix_prefix_functional (s)
  22. 0022specialize cf_convergent_matrix_prefix_functional (x2)
  23. 0023specialize cf_convergent_matrix_prefix_functional (x3)
  24. 0024specialize cf_convergent_matrix_prefix_functional (x6)
  25. 0025specialize cf_convergent_matrix_prefix_functional (x7)
  26. 0026specialize cf_convergent_matrix_prefix_functional (u)
  27. 0027specialize cf_convergent_matrix_prefix_functional (x)
  28. 0028specialize cf_convergent_matrix_prefix_functional (v)
  29. 0029specialize cf_convergent_matrix_prefix_functional (x1)
  30. 0030specialize cf_convergent_matrix_prefix_functional (p)
  31. 0031specialize cf_convergent_matrix_prefix_functional (x4)
  32. 0032specialize cf_convergent_matrix_prefix_functional (q)
  33. 0033specialize cf_convergent_matrix_prefix_functional (x5)
  34. 0034apply cf_convergent_matrix_prefix_functional
  35. 0035exact hc1_witness_witness_witness_witness_right
  36. 0036exact hc2_witness_witness_witness_witness_right
  37. 0037cases heq
  38. 0038cases heq_right
  39. 0039cases heq_right_right
  40. 0040split
  41. 0041exact heq_left
  42. 0042exact heq_right_right_left