BA002C

cf_convergent_old_history_length_transport

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

Equality transport of the actual history length is ordinary substitution, not an index-membership assumption.

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 a b s h e k l. k = l -> (exists cf_gcd_old_length_source. ((((exists ff_h_cf_old_length_source_initial_state. ff_h_cf_old_length_source_initial_state + S (((cf_gcd_old_length_source) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_old_length_source) + (((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_old_length_source_initial_state. h = ff_q_cf_old_length_source_initial_state * S ((S (0)) * e) + (((cf_gcd_old_length_source) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_old_length_source) + (((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_old_length_source_terminal_state. ff_h_cf_old_length_source_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 (k)) * e)) /\ exists ff_q_cf_old_length_source_terminal_state. h = ff_q_cf_old_length_source_terminal_state * S ((S (k)) * 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_old_length_source. (exists ff_lt_cf_old_length_source_index. ff_lt_cf_old_length_source_index + S cf_index_old_length_source = k) -> exists cf_old_a_old_length_source cf_old_b_old_length_source cf_tail_old_length_source cf_new_a_old_length_source cf_new_b_old_length_source cf_head_old_length_source cf_quotient_old_length_source. ((((exists ff_h_cf_old_length_source_previous_state. ff_h_cf_old_length_source_previous_state + S (((cf_old_a_old_length_source) + (((cf_old_b_old_length_source) + (cf_tail_old_length_source)) * S ((cf_old_b_old_length_source) + (cf_tail_old_length_source)) + ((cf_tail_old_length_source) + (cf_tail_old_length_source)))) * S ((cf_old_a_old_length_source) + (((cf_old_b_old_length_source) + (cf_tail_old_length_source)) * S ((cf_old_b_old_length_source) + (cf_tail_old_length_source)) + ((cf_tail_old_length_source) + (cf_tail_old_length_source)))) + ((((cf_old_b_old_length_source) + (cf_tail_old_length_source)) * S ((cf_old_b_old_length_source) + (cf_tail_old_length_source)) + ((cf_tail_old_length_source) + (cf_tail_old_length_source))) + (((cf_old_b_old_length_source) + (cf_tail_old_length_source)) * S ((cf_old_b_old_length_source) + (cf_tail_old_length_source)) + ((cf_tail_old_length_source) + (cf_tail_old_length_source))))) = S ((S (cf_index_old_length_source)) * e)) /\ exists ff_q_cf_old_length_source_previous_state. h = ff_q_cf_old_length_source_previous_state * S ((S (cf_index_old_length_source)) * e) + (((cf_old_a_old_length_source) + (((cf_old_b_old_length_source) + (cf_tail_old_length_source)) * S ((cf_old_b_old_length_source) + (cf_tail_old_length_source)) + ((cf_tail_old_length_source) + (cf_tail_old_length_source)))) * S ((cf_old_a_old_length_source) + (((cf_old_b_old_length_source) + (cf_tail_old_length_source)) * S ((cf_old_b_old_length_source) + (cf_tail_old_length_source)) + ((cf_tail_old_length_source) + (cf_tail_old_length_source)))) + ((((cf_old_b_old_length_source) + (cf_tail_old_length_source)) * S ((cf_old_b_old_length_source) + (cf_tail_old_length_source)) + ((cf_tail_old_length_source) + (cf_tail_old_length_source))) + (((cf_old_b_old_length_source) + (cf_tail_old_length_source)) * S ((cf_old_b_old_length_source) + (cf_tail_old_length_source)) + ((cf_tail_old_length_source) + (cf_tail_old_length_source))))))) /\ ((((exists ff_h_cf_old_length_source_following_state. ff_h_cf_old_length_source_following_state + S (((cf_new_a_old_length_source) + (((cf_new_b_old_length_source) + (cf_head_old_length_source)) * S ((cf_new_b_old_length_source) + (cf_head_old_length_source)) + ((cf_head_old_length_source) + (cf_head_old_length_source)))) * S ((cf_new_a_old_length_source) + (((cf_new_b_old_length_source) + (cf_head_old_length_source)) * S ((cf_new_b_old_length_source) + (cf_head_old_length_source)) + ((cf_head_old_length_source) + (cf_head_old_length_source)))) + ((((cf_new_b_old_length_source) + (cf_head_old_length_source)) * S ((cf_new_b_old_length_source) + (cf_head_old_length_source)) + ((cf_head_old_length_source) + (cf_head_old_length_source))) + (((cf_new_b_old_length_source) + (cf_head_old_length_source)) * S ((cf_new_b_old_length_source) + (cf_head_old_length_source)) + ((cf_head_old_length_source) + (cf_head_old_length_source))))) = S ((S (S cf_index_old_length_source)) * e)) /\ exists ff_q_cf_old_length_source_following_state. h = ff_q_cf_old_length_source_following_state * S ((S (S cf_index_old_length_source)) * e) + (((cf_new_a_old_length_source) + (((cf_new_b_old_length_source) + (cf_head_old_length_source)) * S ((cf_new_b_old_length_source) + (cf_head_old_length_source)) + ((cf_head_old_length_source) + (cf_head_old_length_source)))) * S ((cf_new_a_old_length_source) + (((cf_new_b_old_length_source) + (cf_head_old_length_source)) * S ((cf_new_b_old_length_source) + (cf_head_old_length_source)) + ((cf_head_old_length_source) + (cf_head_old_length_source)))) + ((((cf_new_b_old_length_source) + (cf_head_old_length_source)) * S ((cf_new_b_old_length_source) + (cf_head_old_length_source)) + ((cf_head_old_length_source) + (cf_head_old_length_source))) + (((cf_new_b_old_length_source) + (cf_head_old_length_source)) * S ((cf_new_b_old_length_source) + (cf_head_old_length_source)) + ((cf_head_old_length_source) + (cf_head_old_length_source))))))) /\ (cf_new_b_old_length_source = cf_old_a_old_length_source /\ (cf_new_a_old_length_source = cf_new_b_old_length_source * cf_quotient_old_length_source + cf_old_b_old_length_source /\ ((exists ff_lt_cf_old_length_source_remainder. ff_lt_cf_old_length_source_remainder + S cf_old_b_old_length_source = cf_new_b_old_length_source) /\ (cf_head_old_length_source = S ((cf_quotient_old_length_source + cf_tail_old_length_source) * S (cf_quotient_old_length_source + cf_tail_old_length_source) + (cf_tail_old_length_source + cf_tail_old_length_source))))))))))) -> (exists cf_gcd_old_length_target. ((((exists ff_h_cf_old_length_target_initial_state. ff_h_cf_old_length_target_initial_state + S (((cf_gcd_old_length_target) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_old_length_target) + (((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_old_length_target_initial_state. h = ff_q_cf_old_length_target_initial_state * S ((S (0)) * e) + (((cf_gcd_old_length_target) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_old_length_target) + (((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_old_length_target_terminal_state. ff_h_cf_old_length_target_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_old_length_target_terminal_state. h = ff_q_cf_old_length_target_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_old_length_target. (exists ff_lt_cf_old_length_target_index. ff_lt_cf_old_length_target_index + S cf_index_old_length_target = l) -> exists cf_old_a_old_length_target cf_old_b_old_length_target cf_tail_old_length_target cf_new_a_old_length_target cf_new_b_old_length_target cf_head_old_length_target cf_quotient_old_length_target. ((((exists ff_h_cf_old_length_target_previous_state. ff_h_cf_old_length_target_previous_state + S (((cf_old_a_old_length_target) + (((cf_old_b_old_length_target) + (cf_tail_old_length_target)) * S ((cf_old_b_old_length_target) + (cf_tail_old_length_target)) + ((cf_tail_old_length_target) + (cf_tail_old_length_target)))) * S ((cf_old_a_old_length_target) + (((cf_old_b_old_length_target) + (cf_tail_old_length_target)) * S ((cf_old_b_old_length_target) + (cf_tail_old_length_target)) + ((cf_tail_old_length_target) + (cf_tail_old_length_target)))) + ((((cf_old_b_old_length_target) + (cf_tail_old_length_target)) * S ((cf_old_b_old_length_target) + (cf_tail_old_length_target)) + ((cf_tail_old_length_target) + (cf_tail_old_length_target))) + (((cf_old_b_old_length_target) + (cf_tail_old_length_target)) * S ((cf_old_b_old_length_target) + (cf_tail_old_length_target)) + ((cf_tail_old_length_target) + (cf_tail_old_length_target))))) = S ((S (cf_index_old_length_target)) * e)) /\ exists ff_q_cf_old_length_target_previous_state. h = ff_q_cf_old_length_target_previous_state * S ((S (cf_index_old_length_target)) * e) + (((cf_old_a_old_length_target) + (((cf_old_b_old_length_target) + (cf_tail_old_length_target)) * S ((cf_old_b_old_length_target) + (cf_tail_old_length_target)) + ((cf_tail_old_length_target) + (cf_tail_old_length_target)))) * S ((cf_old_a_old_length_target) + (((cf_old_b_old_length_target) + (cf_tail_old_length_target)) * S ((cf_old_b_old_length_target) + (cf_tail_old_length_target)) + ((cf_tail_old_length_target) + (cf_tail_old_length_target)))) + ((((cf_old_b_old_length_target) + (cf_tail_old_length_target)) * S ((cf_old_b_old_length_target) + (cf_tail_old_length_target)) + ((cf_tail_old_length_target) + (cf_tail_old_length_target))) + (((cf_old_b_old_length_target) + (cf_tail_old_length_target)) * S ((cf_old_b_old_length_target) + (cf_tail_old_length_target)) + ((cf_tail_old_length_target) + (cf_tail_old_length_target))))))) /\ ((((exists ff_h_cf_old_length_target_following_state. ff_h_cf_old_length_target_following_state + S (((cf_new_a_old_length_target) + (((cf_new_b_old_length_target) + (cf_head_old_length_target)) * S ((cf_new_b_old_length_target) + (cf_head_old_length_target)) + ((cf_head_old_length_target) + (cf_head_old_length_target)))) * S ((cf_new_a_old_length_target) + (((cf_new_b_old_length_target) + (cf_head_old_length_target)) * S ((cf_new_b_old_length_target) + (cf_head_old_length_target)) + ((cf_head_old_length_target) + (cf_head_old_length_target)))) + ((((cf_new_b_old_length_target) + (cf_head_old_length_target)) * S ((cf_new_b_old_length_target) + (cf_head_old_length_target)) + ((cf_head_old_length_target) + (cf_head_old_length_target))) + (((cf_new_b_old_length_target) + (cf_head_old_length_target)) * S ((cf_new_b_old_length_target) + (cf_head_old_length_target)) + ((cf_head_old_length_target) + (cf_head_old_length_target))))) = S ((S (S cf_index_old_length_target)) * e)) /\ exists ff_q_cf_old_length_target_following_state. h = ff_q_cf_old_length_target_following_state * S ((S (S cf_index_old_length_target)) * e) + (((cf_new_a_old_length_target) + (((cf_new_b_old_length_target) + (cf_head_old_length_target)) * S ((cf_new_b_old_length_target) + (cf_head_old_length_target)) + ((cf_head_old_length_target) + (cf_head_old_length_target)))) * S ((cf_new_a_old_length_target) + (((cf_new_b_old_length_target) + (cf_head_old_length_target)) * S ((cf_new_b_old_length_target) + (cf_head_old_length_target)) + ((cf_head_old_length_target) + (cf_head_old_length_target)))) + ((((cf_new_b_old_length_target) + (cf_head_old_length_target)) * S ((cf_new_b_old_length_target) + (cf_head_old_length_target)) + ((cf_head_old_length_target) + (cf_head_old_length_target))) + (((cf_new_b_old_length_target) + (cf_head_old_length_target)) * S ((cf_new_b_old_length_target) + (cf_head_old_length_target)) + ((cf_head_old_length_target) + (cf_head_old_length_target))))))) /\ (cf_new_b_old_length_target = cf_old_a_old_length_target /\ (cf_new_a_old_length_target = cf_new_b_old_length_target * cf_quotient_old_length_target + cf_old_b_old_length_target /\ ((exists ff_lt_cf_old_length_target_remainder. ff_lt_cf_old_length_target_remainder + S cf_old_b_old_length_target = cf_new_b_old_length_target) /\ (cf_head_old_length_target = S ((cf_quotient_old_length_target + cf_tail_old_length_target) * S (cf_quotient_old_length_target + cf_tail_old_length_target) + (cf_tail_old_length_target + cf_tail_old_length_target)))))))))))

Constructive proof overview

Generated structural guide

Equality transport of the actual history length is ordinary substitution, not an index-membership assumption.

The unchanged tactic script uses 0 declared prerequisites and contains 13 exact native proof lines.

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

Proof neighborhood

Direct dependencies

none

Direct dependents

BA002D cf_convergent_old_history_nonempty_head BA0047 cf_convergent_full_matrix_is_exact

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

13 script commands · 3 reading checkpoints · 0 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.

01Fix variables and assumptionsL1–9

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro s
  4. L4
    intro h
  5. L5
    intro e
  6. L6
    intro k
  7. L7
    intro l
  8. L8
    intro hl
  9. L9
    intro ht
02Calculate and transport equalitiesL10–12

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

  1. L10
    rewrite <- hl
  2. L11
    rewrite <- hl
  3. L12
    rewrite <- hl
03Use earlier factsL13–13

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

  1. L13
    exact ht

Library-wide reading audit

Original exact command ledger · 13 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro s
  4. 0004intro h
  5. 0005intro e
  6. 0006intro k
  7. 0007intro l
  8. 0008intro hl
  9. 0009intro ht
  10. 0010rewrite <- hl
  11. 0011rewrite <- hl
  12. 0012rewrite <- hl
  13. 0013exact ht