BA0041

continued_fraction_convergent_exists_at_history_index

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

Every genuine in-range index of a G071 history constructs a convergent with proved positive denominator; zero numerators remain allowed.

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 i a b s h e L. (exists cf_gcd_convergent_exists_history. ((((exists ff_h_cf_convergent_exists_history_initial_state. ff_h_cf_convergent_exists_history_initial_state + S (((cf_gcd_convergent_exists_history) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_convergent_exists_history) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * e)) /\ exists ff_q_cf_convergent_exists_history_initial_state. h = ff_q_cf_convergent_exists_history_initial_state * S ((S (0)) * e) + (((cf_gcd_convergent_exists_history) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_convergent_exists_history) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))))) /\ ((((exists ff_h_cf_convergent_exists_history_terminal_state. ff_h_cf_convergent_exists_history_terminal_state + S (((a) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) * S ((a) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) + ((((b) + (s)) * S ((b) + (s)) + ((s) + (s))) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s))))) = S ((S (L)) * e)) /\ exists ff_q_cf_convergent_exists_history_terminal_state. h = ff_q_cf_convergent_exists_history_terminal_state * S ((S (L)) * e) + (((a) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) * S ((a) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) + ((((b) + (s)) * S ((b) + (s)) + ((s) + (s))) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s))))))) /\ forall cf_index_convergent_exists_history. (exists ff_lt_cf_convergent_exists_history_index. ff_lt_cf_convergent_exists_history_index + S cf_index_convergent_exists_history = L) -> exists cf_old_a_convergent_exists_history cf_old_b_convergent_exists_history cf_tail_convergent_exists_history cf_new_a_convergent_exists_history cf_new_b_convergent_exists_history cf_head_convergent_exists_history cf_quotient_convergent_exists_history. ((((exists ff_h_cf_convergent_exists_history_previous_state. ff_h_cf_convergent_exists_history_previous_state + S (((cf_old_a_convergent_exists_history) + (((cf_old_b_convergent_exists_history) + (cf_tail_convergent_exists_history)) * S ((cf_old_b_convergent_exists_history) + (cf_tail_convergent_exists_history)) + ((cf_tail_convergent_exists_history) + (cf_tail_convergent_exists_history)))) * S ((cf_old_a_convergent_exists_history) + (((cf_old_b_convergent_exists_history) + (cf_tail_convergent_exists_history)) * S ((cf_old_b_convergent_exists_history) + (cf_tail_convergent_exists_history)) + ((cf_tail_convergent_exists_history) + (cf_tail_convergent_exists_history)))) + ((((cf_old_b_convergent_exists_history) + (cf_tail_convergent_exists_history)) * S ((cf_old_b_convergent_exists_history) + (cf_tail_convergent_exists_history)) + ((cf_tail_convergent_exists_history) + (cf_tail_convergent_exists_history))) + (((cf_old_b_convergent_exists_history) + (cf_tail_convergent_exists_history)) * S ((cf_old_b_convergent_exists_history) + (cf_tail_convergent_exists_history)) + ((cf_tail_convergent_exists_history) + (cf_tail_convergent_exists_history))))) = S ((S (cf_index_convergent_exists_history)) * e)) /\ exists ff_q_cf_convergent_exists_history_previous_state. h = ff_q_cf_convergent_exists_history_previous_state * S ((S (cf_index_convergent_exists_history)) * e) + (((cf_old_a_convergent_exists_history) + (((cf_old_b_convergent_exists_history) + (cf_tail_convergent_exists_history)) * S ((cf_old_b_convergent_exists_history) + (cf_tail_convergent_exists_history)) + ((cf_tail_convergent_exists_history) + (cf_tail_convergent_exists_history)))) * S ((cf_old_a_convergent_exists_history) + (((cf_old_b_convergent_exists_history) + (cf_tail_convergent_exists_history)) * S ((cf_old_b_convergent_exists_history) + (cf_tail_convergent_exists_history)) + ((cf_tail_convergent_exists_history) + (cf_tail_convergent_exists_history)))) + ((((cf_old_b_convergent_exists_history) + (cf_tail_convergent_exists_history)) * S ((cf_old_b_convergent_exists_history) + (cf_tail_convergent_exists_history)) + ((cf_tail_convergent_exists_history) + (cf_tail_convergent_exists_history))) + (((cf_old_b_convergent_exists_history) + (cf_tail_convergent_exists_history)) * S ((cf_old_b_convergent_exists_history) + (cf_tail_convergent_exists_history)) + ((cf_tail_convergent_exists_history) + (cf_tail_convergent_exists_history))))))) /\ ((((exists ff_h_cf_convergent_exists_history_following_state. ff_h_cf_convergent_exists_history_following_state + S (((cf_new_a_convergent_exists_history) + (((cf_new_b_convergent_exists_history) + (cf_head_convergent_exists_history)) * S ((cf_new_b_convergent_exists_history) + (cf_head_convergent_exists_history)) + ((cf_head_convergent_exists_history) + (cf_head_convergent_exists_history)))) * S ((cf_new_a_convergent_exists_history) + (((cf_new_b_convergent_exists_history) + (cf_head_convergent_exists_history)) * S ((cf_new_b_convergent_exists_history) + (cf_head_convergent_exists_history)) + ((cf_head_convergent_exists_history) + (cf_head_convergent_exists_history)))) + ((((cf_new_b_convergent_exists_history) + (cf_head_convergent_exists_history)) * S ((cf_new_b_convergent_exists_history) + (cf_head_convergent_exists_history)) + ((cf_head_convergent_exists_history) + (cf_head_convergent_exists_history))) + (((cf_new_b_convergent_exists_history) + (cf_head_convergent_exists_history)) * S ((cf_new_b_convergent_exists_history) + (cf_head_convergent_exists_history)) + ((cf_head_convergent_exists_history) + (cf_head_convergent_exists_history))))) = S ((S (S cf_index_convergent_exists_history)) * e)) /\ exists ff_q_cf_convergent_exists_history_following_state. h = ff_q_cf_convergent_exists_history_following_state * S ((S (S cf_index_convergent_exists_history)) * e) + (((cf_new_a_convergent_exists_history) + (((cf_new_b_convergent_exists_history) + (cf_head_convergent_exists_history)) * S ((cf_new_b_convergent_exists_history) + (cf_head_convergent_exists_history)) + ((cf_head_convergent_exists_history) + (cf_head_convergent_exists_history)))) * S ((cf_new_a_convergent_exists_history) + (((cf_new_b_convergent_exists_history) + (cf_head_convergent_exists_history)) * S ((cf_new_b_convergent_exists_history) + (cf_head_convergent_exists_history)) + ((cf_head_convergent_exists_history) + (cf_head_convergent_exists_history)))) + ((((cf_new_b_convergent_exists_history) + (cf_head_convergent_exists_history)) * S ((cf_new_b_convergent_exists_history) + (cf_head_convergent_exists_history)) + ((cf_head_convergent_exists_history) + (cf_head_convergent_exists_history))) + (((cf_new_b_convergent_exists_history) + (cf_head_convergent_exists_history)) * S ((cf_new_b_convergent_exists_history) + (cf_head_convergent_exists_history)) + ((cf_head_convergent_exists_history) + (cf_head_convergent_exists_history))))))) /\ (cf_new_b_convergent_exists_history = cf_old_a_convergent_exists_history /\ (cf_new_a_convergent_exists_history = cf_new_b_convergent_exists_history * cf_quotient_convergent_exists_history + cf_old_b_convergent_exists_history /\ ((exists ff_lt_cf_convergent_exists_history_remainder. ff_lt_cf_convergent_exists_history_remainder + S cf_old_b_convergent_exists_history = cf_new_b_convergent_exists_history) /\ (cf_head_convergent_exists_history = S ((cf_quotient_convergent_exists_history + cf_tail_convergent_exists_history) * S (cf_quotient_convergent_exists_history + cf_tail_convergent_exists_history) + (cf_tail_convergent_exists_history + cf_tail_convergent_exists_history))))))))))) -> (exists cfba_gap_convergent_exists_index. cfba_gap_convergent_exists_index + S (i) = (L)) -> exists u v. (exists cfc_previous_numerator_existing_convergent cfc_previous_denominator_existing_convergent cfc_code_existing_convergent cfc_scale_existing_convergent. ((~(v = 0)) /\ (exists cfc_tail_existing_convergentcomputation. ((exists cfc_state_existing_convergentcomputationinitial. ((exists cfc_left_existing_convergentcomputationinitialcode cfc_right_existing_convergentcomputationinitialcode cfc_matrix_existing_convergentcomputationinitialcode. ((cfc_left_existing_convergentcomputationinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_existing_convergentcomputationinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_existing_convergentcomputationinitialcode = ((cfc_left_existing_convergentcomputationinitialcode) + (cfc_right_existing_convergentcomputationinitialcode)) * S ((cfc_left_existing_convergentcomputationinitialcode) + (cfc_right_existing_convergentcomputationinitialcode)) + ((cfc_right_existing_convergentcomputationinitialcode) + (cfc_right_existing_convergentcomputationinitialcode))) /\ ((cfc_state_existing_convergentcomputationinitial) = ((cfc_tail_existing_convergentcomputation) + (cfc_matrix_existing_convergentcomputationinitialcode)) * S ((cfc_tail_existing_convergentcomputation) + (cfc_matrix_existing_convergentcomputationinitialcode)) + ((cfc_matrix_existing_convergentcomputationinitialcode) + (cfc_matrix_existing_convergentcomputationinitialcode))))))) /\ (((exists ff_h_existing_convergentcomputationinitialentry. ff_h_existing_convergentcomputationinitialentry + S (cfc_state_existing_convergentcomputationinitial) = S ((S (0)) * cfc_scale_existing_convergent)) /\ exists ff_q_existing_convergentcomputationinitialentry. cfc_code_existing_convergent = ff_q_existing_convergentcomputationinitialentry * S ((S (0)) * cfc_scale_existing_convergent) + (cfc_state_existing_convergentcomputationinitial))))) /\ ((exists cfc_state_existing_convergentcomputationterminal. ((exists cfc_left_existing_convergentcomputationterminalcode cfc_right_existing_convergentcomputationterminalcode cfc_matrix_existing_convergentcomputationterminalcode. ((cfc_left_existing_convergentcomputationterminalcode = ((u) + (cfc_previous_numerator_existing_convergent)) * S ((u) + (cfc_previous_numerator_existing_convergent)) + ((cfc_previous_numerator_existing_convergent) + (cfc_previous_numerator_existing_convergent))) /\ ((cfc_right_existing_convergentcomputationterminalcode = ((v) + (cfc_previous_denominator_existing_convergent)) * S ((v) + (cfc_previous_denominator_existing_convergent)) + ((cfc_previous_denominator_existing_convergent) + (cfc_previous_denominator_existing_convergent))) /\ ((cfc_matrix_existing_convergentcomputationterminalcode = ((cfc_left_existing_convergentcomputationterminalcode) + (cfc_right_existing_convergentcomputationterminalcode)) * S ((cfc_left_existing_convergentcomputationterminalcode) + (cfc_right_existing_convergentcomputationterminalcode)) + ((cfc_right_existing_convergentcomputationterminalcode) + (cfc_right_existing_convergentcomputationterminalcode))) /\ ((cfc_state_existing_convergentcomputationterminal) = ((s) + (cfc_matrix_existing_convergentcomputationterminalcode)) * S ((s) + (cfc_matrix_existing_convergentcomputationterminalcode)) + ((cfc_matrix_existing_convergentcomputationterminalcode) + (cfc_matrix_existing_convergentcomputationterminalcode))))))) /\ (((exists ff_h_existing_convergentcomputationterminalentry. ff_h_existing_convergentcomputationterminalentry + S (cfc_state_existing_convergentcomputationterminal) = S ((S (S (i))) * cfc_scale_existing_convergent)) /\ exists ff_q_existing_convergentcomputationterminalentry. cfc_code_existing_convergent = ff_q_existing_convergentcomputationterminalentry * S ((S (S (i))) * cfc_scale_existing_convergent) + (cfc_state_existing_convergentcomputationterminal))))) /\ (forall cfc_index_existing_convergentcomputation. (exists cfba_gap_existing_convergentcomputationbound. cfba_gap_existing_convergentcomputationbound + S (cfc_index_existing_convergentcomputation) = (S (i))) -> exists cfc_old_existing_convergentcomputation cfc_a_existing_convergentcomputation cfc_b_existing_convergentcomputation cfc_c_existing_convergentcomputation cfc_d_existing_convergentcomputation cfc_new_existing_convergentcomputation cfc_quotient_existing_convergentcomputation. ((exists cfc_state_existing_convergentcomputationprevious. ((exists cfc_left_existing_convergentcomputationpreviouscode cfc_right_existing_convergentcomputationpreviouscode cfc_matrix_existing_convergentcomputationpreviouscode. ((cfc_left_existing_convergentcomputationpreviouscode = ((cfc_a_existing_convergentcomputation) + (cfc_b_existing_convergentcomputation)) * S ((cfc_a_existing_convergentcomputation) + (cfc_b_existing_convergentcomputation)) + ((cfc_b_existing_convergentcomputation) + (cfc_b_existing_convergentcomputation))) /\ ((cfc_right_existing_convergentcomputationpreviouscode = ((cfc_c_existing_convergentcomputation) + (cfc_d_existing_convergentcomputation)) * S ((cfc_c_existing_convergentcomputation) + (cfc_d_existing_convergentcomputation)) + ((cfc_d_existing_convergentcomputation) + (cfc_d_existing_convergentcomputation))) /\ ((cfc_matrix_existing_convergentcomputationpreviouscode = ((cfc_left_existing_convergentcomputationpreviouscode) + (cfc_right_existing_convergentcomputationpreviouscode)) * S ((cfc_left_existing_convergentcomputationpreviouscode) + (cfc_right_existing_convergentcomputationpreviouscode)) + ((cfc_right_existing_convergentcomputationpreviouscode) + (cfc_right_existing_convergentcomputationpreviouscode))) /\ ((cfc_state_existing_convergentcomputationprevious) = ((cfc_old_existing_convergentcomputation) + (cfc_matrix_existing_convergentcomputationpreviouscode)) * S ((cfc_old_existing_convergentcomputation) + (cfc_matrix_existing_convergentcomputationpreviouscode)) + ((cfc_matrix_existing_convergentcomputationpreviouscode) + (cfc_matrix_existing_convergentcomputationpreviouscode))))))) /\ (((exists ff_h_existing_convergentcomputationpreviousentry. ff_h_existing_convergentcomputationpreviousentry + S (cfc_state_existing_convergentcomputationprevious) = S ((S (cfc_index_existing_convergentcomputation)) * cfc_scale_existing_convergent)) /\ exists ff_q_existing_convergentcomputationpreviousentry. cfc_code_existing_convergent = ff_q_existing_convergentcomputationpreviousentry * S ((S (cfc_index_existing_convergentcomputation)) * cfc_scale_existing_convergent) + (cfc_state_existing_convergentcomputationprevious))))) /\ ((exists cfc_state_existing_convergentcomputationfollowing. ((exists cfc_left_existing_convergentcomputationfollowingcode cfc_right_existing_convergentcomputationfollowingcode cfc_matrix_existing_convergentcomputationfollowingcode. ((cfc_left_existing_convergentcomputationfollowingcode = (((cfc_quotient_existing_convergentcomputation * cfc_a_existing_convergentcomputation + cfc_c_existing_convergentcomputation)) + ((cfc_quotient_existing_convergentcomputation * cfc_b_existing_convergentcomputation + cfc_d_existing_convergentcomputation))) * S (((cfc_quotient_existing_convergentcomputation * cfc_a_existing_convergentcomputation + cfc_c_existing_convergentcomputation)) + ((cfc_quotient_existing_convergentcomputation * cfc_b_existing_convergentcomputation + cfc_d_existing_convergentcomputation))) + (((cfc_quotient_existing_convergentcomputation * cfc_b_existing_convergentcomputation + cfc_d_existing_convergentcomputation)) + ((cfc_quotient_existing_convergentcomputation * cfc_b_existing_convergentcomputation + cfc_d_existing_convergentcomputation)))) /\ ((cfc_right_existing_convergentcomputationfollowingcode = ((cfc_a_existing_convergentcomputation) + (cfc_b_existing_convergentcomputation)) * S ((cfc_a_existing_convergentcomputation) + (cfc_b_existing_convergentcomputation)) + ((cfc_b_existing_convergentcomputation) + (cfc_b_existing_convergentcomputation))) /\ ((cfc_matrix_existing_convergentcomputationfollowingcode = ((cfc_left_existing_convergentcomputationfollowingcode) + (cfc_right_existing_convergentcomputationfollowingcode)) * S ((cfc_left_existing_convergentcomputationfollowingcode) + (cfc_right_existing_convergentcomputationfollowingcode)) + ((cfc_right_existing_convergentcomputationfollowingcode) + (cfc_right_existing_convergentcomputationfollowingcode))) /\ ((cfc_state_existing_convergentcomputationfollowing) = ((cfc_new_existing_convergentcomputation) + (cfc_matrix_existing_convergentcomputationfollowingcode)) * S ((cfc_new_existing_convergentcomputation) + (cfc_matrix_existing_convergentcomputationfollowingcode)) + ((cfc_matrix_existing_convergentcomputationfollowingcode) + (cfc_matrix_existing_convergentcomputationfollowingcode))))))) /\ (((exists ff_h_existing_convergentcomputationfollowingentry. ff_h_existing_convergentcomputationfollowingentry + S (cfc_state_existing_convergentcomputationfollowing) = S ((S (S cfc_index_existing_convergentcomputation)) * cfc_scale_existing_convergent)) /\ exists ff_q_existing_convergentcomputationfollowingentry. cfc_code_existing_convergent = ff_q_existing_convergentcomputationfollowingentry * S ((S (S cfc_index_existing_convergentcomputation)) * cfc_scale_existing_convergent) + (cfc_state_existing_convergentcomputationfollowing))))) /\ (cfc_new_existing_convergentcomputation = S ((cfc_quotient_existing_convergentcomputation + cfc_old_existing_convergentcomputation) * S (cfc_quotient_existing_convergentcomputation + cfc_old_existing_convergentcomputation) + (cfc_old_existing_convergentcomputation + cfc_old_existing_convergentcomputation)))))))))))

Constructive proof overview

Generated structural guide

Every genuine in-range index of a G071 history constructs a convergent with proved positive denominator; zero numerators remain allowed.

The unchanged tactic script uses 3 declared prerequisites and contains 59 exact native proof lines.

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

Proof neighborhood

Direct dependencies

BA003F cf_convergent_every_valid_matrix_prefix_exists BA000D cf_approximation_derived_invariant_denominator_positive BA003E cf_convergent_actual_prefix_error_invariant

Direct dependents

BA0049 continued_fraction_exact_terminal_convergent_exists BA004D continued_fraction_convergent_exists_unique_at_history_index

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

59 script commands · 10 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.

Named ingredients (3)
cf convergent every valid matrix prefix existscf approximation derived invariant denominator positivecf convergent actual prefix error invariant

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–9

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

  1. L1
    intro i
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro s
  5. L5
    intro h
  6. L6
    intro e
  7. L7
    intro L
  8. L8
    intro ht
  9. L9
    intro hi
02Establish hpL10–19

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

  1. L10
    have hp : ∃ cfc_h_convergent_exists_matrix. ∃ cfc_e_convergent_exists_matrix. ∃ cfc_u_convergent_exists_matrix. ∃ cfc_U_convergent_exists_matrix. ∃ cfc_v_convergent_exists_matrix. ∃ cfc_V_convergent_exists_matrix. ConvergentMatrixTrace(s,cfc_h_convergent_exists_matrix,cfc_e_convergent_exists_matrix,S i,cfc_u_convergent_exists_matrix,cfc_U_convergent_exists_matrix,cfc_v_convergent_exists_matrix,cfc_V_convergent_exists_matrix)Definitions: ConvergentMatrixTrace
  2. L11
    specialize cf_convergent_every_valid_matrix_prefix_exists (L)
  3. L12
    specialize cf_convergent_every_valid_matrix_prefix_exists (S i)
  4. L13
    specialize cf_convergent_every_valid_matrix_prefix_exists (a)
  5. L14
    specialize cf_convergent_every_valid_matrix_prefix_exists (b)
  6. L15
    specialize cf_convergent_every_valid_matrix_prefix_exists (s)
  7. L16
    specialize cf_convergent_every_valid_matrix_prefix_exists (h)
  8. L17
    specialize cf_convergent_every_valid_matrix_prefix_exists (e)
  9. L18
    apply cf_convergent_every_valid_matrix_prefix_exists
  10. L19
    exact ht
03Use earlier factsL20–20

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

  1. L20
    exact hi
04Separate the logical casesL21–26

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

  1. L21
    cases hp
  2. L22
    cases hp_witness
  3. L23
    cases hp_witness_witness
  4. L24
    cases hp_witness_witness_witness
  5. L25
    cases hp_witness_witness_witness_witness
  6. L26
    cases hp_witness_witness_witness_witness_witness
05Construct an explicit witnessL27–32

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

  1. L27
    exists x2
  2. L28
    exists x4
  3. L29
    exists x3
  4. L30
    exists x5
  5. L31
    exists x
  6. L32
    exists x1
06Separate the logical casesL33–33

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

  1. L33
    split
07Fix variables and assumptionsL34–34

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

  1. L34
    intro hz
08Use earlier factsL35–44

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

  1. L35
    specialize cf_approximation_derived_invariant_denominator_positive (a)
  2. L36
    specialize cf_approximation_derived_invariant_denominator_positive (b)
  3. L37
    specialize cf_approximation_derived_invariant_denominator_positive (x2)
  4. L38
    specialize cf_approximation_derived_invariant_denominator_positive (x3)
  5. L39
    specialize cf_approximation_derived_invariant_denominator_positive (x4)
  6. L40
    specialize cf_approximation_derived_invariant_denominator_positive (x5)
  7. L41
    apply cf_approximation_derived_invariant_denominator_positive
  8. L42
    specialize cf_convergent_actual_prefix_error_invariant (i)
  9. L43
    specialize cf_convergent_actual_prefix_error_invariant (a)
  10. L44
    specialize cf_convergent_actual_prefix_error_invariant (b)
09Use earlier factsL45–54

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

  1. L45
    specialize cf_convergent_actual_prefix_error_invariant (s)
  2. L46
    specialize cf_convergent_actual_prefix_error_invariant (h)
  3. L47
    specialize cf_convergent_actual_prefix_error_invariant (e)
  4. L48
    specialize cf_convergent_actual_prefix_error_invariant (L)
  5. L49
    specialize cf_convergent_actual_prefix_error_invariant (x)
  6. L50
    specialize cf_convergent_actual_prefix_error_invariant (x1)
  7. L51
    specialize cf_convergent_actual_prefix_error_invariant (x2)
  8. L52
    specialize cf_convergent_actual_prefix_error_invariant (x3)
  9. L53
    specialize cf_convergent_actual_prefix_error_invariant (x4)
  10. L54
    specialize cf_convergent_actual_prefix_error_invariant (x5)
10Use earlier factsL55–59

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

  1. L55
    apply cf_convergent_actual_prefix_error_invariant
  2. L56
    exact ht
  3. L57
    exact hp_witness_witness_witness_witness_witness_witness
  4. L58
    exact hz
  5. L59
    exact hp_witness_witness_witness_witness_witness_witness

Library-wide reading audit

Original exact command ledger · 59 lines
  1. 0001intro i
  2. 0002intro a
  3. 0003intro b
  4. 0004intro s
  5. 0005intro h
  6. 0006intro e
  7. 0007intro L
  8. 0008intro ht
  9. 0009intro hi
  10. 0010have hp : exists cfc_h_convergent_exists_matrix cfc_e_convergent_exists_matrix cfc_u_convergent_exists_matrix cfc_U_convergent_exists_matrix cfc_v_convergent_exists_matrix cfc_V_convergent_exists_matrix. exists cfc_tail_convergent_exists_matrixbody. ((exists cfc_state_convergent_exists_matrixbodyinitial. ((exists cfc_left_convergent_exists_matrixbodyinitialcode cfc_right_convergent_exists_matrixbodyinitialcode cfc_matrix_convergent_exists_matrixbodyinitialcode. ((cfc_left_convergent_exists_matrixbodyinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_convergent_exists_matrixbodyinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_convergent_exists_matrixbodyinitialcode = ((cfc_left_convergent_exists_matrixbodyinitialcode) + (cfc_right_convergent_exists_matrixbodyinitialcode)) * S ((cfc_left_convergent_exists_matrixbodyinitialcode) + (cfc_right_convergent_exists_matrixbodyinitialcode)) + ((cfc_right_convergent_exists_matrixbodyinitialcode) + (cfc_right_convergent_exists_matrixbodyinitialcode))) /\ ((cfc_state_convergent_exists_matrixbodyinitial) = ((cfc_tail_convergent_exists_matrixbody) + (cfc_matrix_convergent_exists_matrixbodyinitialcode)) * S ((cfc_tail_convergent_exists_matrixbody) + (cfc_matrix_convergent_exists_matrixbodyinitialcode)) + ((cfc_matrix_convergent_exists_matrixbodyinitialcode) + (cfc_matrix_convergent_exists_matrixbodyinitialcode))))))) /\ (((exists ff_h_convergent_exists_matrixbodyinitialentry. ff_h_convergent_exists_matrixbodyinitialentry + S (cfc_state_convergent_exists_matrixbodyinitial) = S ((S (0)) * cfc_e_convergent_exists_matrix)) /\ exists ff_q_convergent_exists_matrixbodyinitialentry. cfc_h_convergent_exists_matrix = ff_q_convergent_exists_matrixbodyinitialentry * S ((S (0)) * cfc_e_convergent_exists_matrix) + (cfc_state_convergent_exists_matrixbodyinitial))))) /\ ((exists cfc_state_convergent_exists_matrixbodyterminal. ((exists cfc_left_convergent_exists_matrixbodyterminalcode cfc_right_convergent_exists_matrixbodyterminalcode cfc_matrix_convergent_exists_matrixbodyterminalcode. ((cfc_left_convergent_exists_matrixbodyterminalcode = ((cfc_u_convergent_exists_matrix) + (cfc_U_convergent_exists_matrix)) * S ((cfc_u_convergent_exists_matrix) + (cfc_U_convergent_exists_matrix)) + ((cfc_U_convergent_exists_matrix) + (cfc_U_convergent_exists_matrix))) /\ ((cfc_right_convergent_exists_matrixbodyterminalcode = ((cfc_v_convergent_exists_matrix) + (cfc_V_convergent_exists_matrix)) * S ((cfc_v_convergent_exists_matrix) + (cfc_V_convergent_exists_matrix)) + ((cfc_V_convergent_exists_matrix) + (cfc_V_convergent_exists_matrix))) /\ ((cfc_matrix_convergent_exists_matrixbodyterminalcode = ((cfc_left_convergent_exists_matrixbodyterminalcode) + (cfc_right_convergent_exists_matrixbodyterminalcode)) * S ((cfc_left_convergent_exists_matrixbodyterminalcode) + (cfc_right_convergent_exists_matrixbodyterminalcode)) + ((cfc_right_convergent_exists_matrixbodyterminalcode) + (cfc_right_convergent_exists_matrixbodyterminalcode))) /\ ((cfc_state_convergent_exists_matrixbodyterminal) = ((s) + (cfc_matrix_convergent_exists_matrixbodyterminalcode)) * S ((s) + (cfc_matrix_convergent_exists_matrixbodyterminalcode)) + ((cfc_matrix_convergent_exists_matrixbodyterminalcode) + (cfc_matrix_convergent_exists_matrixbodyterminalcode))))))) /\ (((exists ff_h_convergent_exists_matrixbodyterminalentry. ff_h_convergent_exists_matrixbodyterminalentry + S (cfc_state_convergent_exists_matrixbodyterminal) = S ((S (S i)) * cfc_e_convergent_exists_matrix)) /\ exists ff_q_convergent_exists_matrixbodyterminalentry. cfc_h_convergent_exists_matrix = ff_q_convergent_exists_matrixbodyterminalentry * S ((S (S i)) * cfc_e_convergent_exists_matrix) + (cfc_state_convergent_exists_matrixbodyterminal))))) /\ (forall cfc_index_convergent_exists_matrixbody. (exists cfba_gap_convergent_exists_matrixbodybound. cfba_gap_convergent_exists_matrixbodybound + S (cfc_index_convergent_exists_matrixbody) = (S i)) -> exists cfc_old_convergent_exists_matrixbody cfc_a_convergent_exists_matrixbody cfc_b_convergent_exists_matrixbody cfc_c_convergent_exists_matrixbody cfc_d_convergent_exists_matrixbody cfc_new_convergent_exists_matrixbody cfc_quotient_convergent_exists_matrixbody. ((exists cfc_state_convergent_exists_matrixbodyprevious. ((exists cfc_left_convergent_exists_matrixbodypreviouscode cfc_right_convergent_exists_matrixbodypreviouscode cfc_matrix_convergent_exists_matrixbodypreviouscode. ((cfc_left_convergent_exists_matrixbodypreviouscode = ((cfc_a_convergent_exists_matrixbody) + (cfc_b_convergent_exists_matrixbody)) * S ((cfc_a_convergent_exists_matrixbody) + (cfc_b_convergent_exists_matrixbody)) + ((cfc_b_convergent_exists_matrixbody) + (cfc_b_convergent_exists_matrixbody))) /\ ((cfc_right_convergent_exists_matrixbodypreviouscode = ((cfc_c_convergent_exists_matrixbody) + (cfc_d_convergent_exists_matrixbody)) * S ((cfc_c_convergent_exists_matrixbody) + (cfc_d_convergent_exists_matrixbody)) + ((cfc_d_convergent_exists_matrixbody) + (cfc_d_convergent_exists_matrixbody))) /\ ((cfc_matrix_convergent_exists_matrixbodypreviouscode = ((cfc_left_convergent_exists_matrixbodypreviouscode) + (cfc_right_convergent_exists_matrixbodypreviouscode)) * S ((cfc_left_convergent_exists_matrixbodypreviouscode) + (cfc_right_convergent_exists_matrixbodypreviouscode)) + ((cfc_right_convergent_exists_matrixbodypreviouscode) + (cfc_right_convergent_exists_matrixbodypreviouscode))) /\ ((cfc_state_convergent_exists_matrixbodyprevious) = ((cfc_old_convergent_exists_matrixbody) + (cfc_matrix_convergent_exists_matrixbodypreviouscode)) * S ((cfc_old_convergent_exists_matrixbody) + (cfc_matrix_convergent_exists_matrixbodypreviouscode)) + ((cfc_matrix_convergent_exists_matrixbodypreviouscode) + (cfc_matrix_convergent_exists_matrixbodypreviouscode))))))) /\ (((exists ff_h_convergent_exists_matrixbodypreviousentry. ff_h_convergent_exists_matrixbodypreviousentry + S (cfc_state_convergent_exists_matrixbodyprevious) = S ((S (cfc_index_convergent_exists_matrixbody)) * cfc_e_convergent_exists_matrix)) /\ exists ff_q_convergent_exists_matrixbodypreviousentry. cfc_h_convergent_exists_matrix = ff_q_convergent_exists_matrixbodypreviousentry * S ((S (cfc_index_convergent_exists_matrixbody)) * cfc_e_convergent_exists_matrix) + (cfc_state_convergent_exists_matrixbodyprevious))))) /\ ((exists cfc_state_convergent_exists_matrixbodyfollowing. ((exists cfc_left_convergent_exists_matrixbodyfollowingcode cfc_right_convergent_exists_matrixbodyfollowingcode cfc_matrix_convergent_exists_matrixbodyfollowingcode. ((cfc_left_convergent_exists_matrixbodyfollowingcode = (((cfc_quotient_convergent_exists_matrixbody * cfc_a_convergent_exists_matrixbody + cfc_c_convergent_exists_matrixbody)) + ((cfc_quotient_convergent_exists_matrixbody * cfc_b_convergent_exists_matrixbody + cfc_d_convergent_exists_matrixbody))) * S (((cfc_quotient_convergent_exists_matrixbody * cfc_a_convergent_exists_matrixbody + cfc_c_convergent_exists_matrixbody)) + ((cfc_quotient_convergent_exists_matrixbody * cfc_b_convergent_exists_matrixbody + cfc_d_convergent_exists_matrixbody))) + (((cfc_quotient_convergent_exists_matrixbody * cfc_b_convergent_exists_matrixbody + cfc_d_convergent_exists_matrixbody)) + ((cfc_quotient_convergent_exists_matrixbody * cfc_b_convergent_exists_matrixbody + cfc_d_convergent_exists_matrixbody)))) /\ ((cfc_right_convergent_exists_matrixbodyfollowingcode = ((cfc_a_convergent_exists_matrixbody) + (cfc_b_convergent_exists_matrixbody)) * S ((cfc_a_convergent_exists_matrixbody) + (cfc_b_convergent_exists_matrixbody)) + ((cfc_b_convergent_exists_matrixbody) + (cfc_b_convergent_exists_matrixbody))) /\ ((cfc_matrix_convergent_exists_matrixbodyfollowingcode = ((cfc_left_convergent_exists_matrixbodyfollowingcode) + (cfc_right_convergent_exists_matrixbodyfollowingcode)) * S ((cfc_left_convergent_exists_matrixbodyfollowingcode) + (cfc_right_convergent_exists_matrixbodyfollowingcode)) + ((cfc_right_convergent_exists_matrixbodyfollowingcode) + (cfc_right_convergent_exists_matrixbodyfollowingcode))) /\ ((cfc_state_convergent_exists_matrixbodyfollowing) = ((cfc_new_convergent_exists_matrixbody) + (cfc_matrix_convergent_exists_matrixbodyfollowingcode)) * S ((cfc_new_convergent_exists_matrixbody) + (cfc_matrix_convergent_exists_matrixbodyfollowingcode)) + ((cfc_matrix_convergent_exists_matrixbodyfollowingcode) + (cfc_matrix_convergent_exists_matrixbodyfollowingcode))))))) /\ (((exists ff_h_convergent_exists_matrixbodyfollowingentry. ff_h_convergent_exists_matrixbodyfollowingentry + S (cfc_state_convergent_exists_matrixbodyfollowing) = S ((S (S cfc_index_convergent_exists_matrixbody)) * cfc_e_convergent_exists_matrix)) /\ exists ff_q_convergent_exists_matrixbodyfollowingentry. cfc_h_convergent_exists_matrix = ff_q_convergent_exists_matrixbodyfollowingentry * S ((S (S cfc_index_convergent_exists_matrixbody)) * cfc_e_convergent_exists_matrix) + (cfc_state_convergent_exists_matrixbodyfollowing))))) /\ (cfc_new_convergent_exists_matrixbody = S ((cfc_quotient_convergent_exists_matrixbody + cfc_old_convergent_exists_matrixbody) * S (cfc_quotient_convergent_exists_matrixbody + cfc_old_convergent_exists_matrixbody) + (cfc_old_convergent_exists_matrixbody + cfc_old_convergent_exists_matrixbody))))))))
  11. 0011specialize cf_convergent_every_valid_matrix_prefix_exists (L)
  12. 0012specialize cf_convergent_every_valid_matrix_prefix_exists (S i)
  13. 0013specialize cf_convergent_every_valid_matrix_prefix_exists (a)
  14. 0014specialize cf_convergent_every_valid_matrix_prefix_exists (b)
  15. 0015specialize cf_convergent_every_valid_matrix_prefix_exists (s)
  16. 0016specialize cf_convergent_every_valid_matrix_prefix_exists (h)
  17. 0017specialize cf_convergent_every_valid_matrix_prefix_exists (e)
  18. 0018apply cf_convergent_every_valid_matrix_prefix_exists
  19. 0019exact ht
  20. 0020exact hi
  21. 0021cases hp
  22. 0022cases hp_witness
  23. 0023cases hp_witness_witness
  24. 0024cases hp_witness_witness_witness
  25. 0025cases hp_witness_witness_witness_witness
  26. 0026cases hp_witness_witness_witness_witness_witness
  27. 0027exists x2
  28. 0028exists x4
  29. 0029exists x3
  30. 0030exists x5
  31. 0031exists x
  32. 0032exists x1
  33. 0033split
  34. 0034intro hz
  35. 0035specialize cf_approximation_derived_invariant_denominator_positive (a)
  36. 0036specialize cf_approximation_derived_invariant_denominator_positive (b)
  37. 0037specialize cf_approximation_derived_invariant_denominator_positive (x2)
  38. 0038specialize cf_approximation_derived_invariant_denominator_positive (x3)
  39. 0039specialize cf_approximation_derived_invariant_denominator_positive (x4)
  40. 0040specialize cf_approximation_derived_invariant_denominator_positive (x5)
  41. 0041apply cf_approximation_derived_invariant_denominator_positive
  42. 0042specialize cf_convergent_actual_prefix_error_invariant (i)
  43. 0043specialize cf_convergent_actual_prefix_error_invariant (a)
  44. 0044specialize cf_convergent_actual_prefix_error_invariant (b)
  45. 0045specialize cf_convergent_actual_prefix_error_invariant (s)
  46. 0046specialize cf_convergent_actual_prefix_error_invariant (h)
  47. 0047specialize cf_convergent_actual_prefix_error_invariant (e)
  48. 0048specialize cf_convergent_actual_prefix_error_invariant (L)
  49. 0049specialize cf_convergent_actual_prefix_error_invariant (x)
  50. 0050specialize cf_convergent_actual_prefix_error_invariant (x1)
  51. 0051specialize cf_convergent_actual_prefix_error_invariant (x2)
  52. 0052specialize cf_convergent_actual_prefix_error_invariant (x3)
  53. 0053specialize cf_convergent_actual_prefix_error_invariant (x4)
  54. 0054specialize cf_convergent_actual_prefix_error_invariant (x5)
  55. 0055apply cf_convergent_actual_prefix_error_invariant
  56. 0056exact ht
  57. 0057exact hp_witness_witness_witness_witness_witness_witness
  58. 0058exact hz
  59. 0059exact hp_witness_witness_witness_witness_witness_witness