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 t h e k u U v V. s = t -> (exists cfc_tail_list_source. ((exists cfc_state_list_sourceinitial. ((exists cfc_left_list_sourceinitialcode cfc_right_list_sourceinitialcode cfc_matrix_list_sourceinitialcode. ((cfc_left_list_sourceinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_list_sourceinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_list_sourceinitialcode = ((cfc_left_list_sourceinitialcode) + (cfc_right_list_sourceinitialcode)) * S ((cfc_left_list_sourceinitialcode) + (cfc_right_list_sourceinitialcode)) + ((cfc_right_list_sourceinitialcode) + (cfc_right_list_sourceinitialcode))) /\ ((cfc_state_list_sourceinitial) = ((cfc_tail_list_source) + (cfc_matrix_list_sourceinitialcode)) * S ((cfc_tail_list_source) + (cfc_matrix_list_sourceinitialcode)) + ((cfc_matrix_list_sourceinitialcode) + (cfc_matrix_list_sourceinitialcode))))))) /\ (((exists ff_h_list_sourceinitialentry. ff_h_list_sourceinitialentry + S (cfc_state_list_sourceinitial) = S ((S (0)) * e)) /\ exists ff_q_list_sourceinitialentry. h = ff_q_list_sourceinitialentry * S ((S (0)) * e) + (cfc_state_list_sourceinitial))))) /\ ((exists cfc_state_list_sourceterminal. ((exists cfc_left_list_sourceterminalcode cfc_right_list_sourceterminalcode cfc_matrix_list_sourceterminalcode. ((cfc_left_list_sourceterminalcode = ((u) + (U)) * S ((u) + (U)) + ((U) + (U))) /\ ((cfc_right_list_sourceterminalcode = ((v) + (V)) * S ((v) + (V)) + ((V) + (V))) /\ ((cfc_matrix_list_sourceterminalcode = ((cfc_left_list_sourceterminalcode) + (cfc_right_list_sourceterminalcode)) * S ((cfc_left_list_sourceterminalcode) + (cfc_right_list_sourceterminalcode)) + ((cfc_right_list_sourceterminalcode) + (cfc_right_list_sourceterminalcode))) /\ ((cfc_state_list_sourceterminal) = ((s) + (cfc_matrix_list_sourceterminalcode)) * S ((s) + (cfc_matrix_list_sourceterminalcode)) + ((cfc_matrix_list_sourceterminalcode) + (cfc_matrix_list_sourceterminalcode))))))) /\ (((exists ff_h_list_sourceterminalentry. ff_h_list_sourceterminalentry + S (cfc_state_list_sourceterminal) = S ((S (k)) * e)) /\ exists ff_q_list_sourceterminalentry. h = ff_q_list_sourceterminalentry * S ((S (k)) * e) + (cfc_state_list_sourceterminal))))) /\ (forall cfc_index_list_source. (exists cfba_gap_list_sourcebound. cfba_gap_list_sourcebound + S (cfc_index_list_source) = (k)) -> exists cfc_old_list_source cfc_a_list_source cfc_b_list_source cfc_c_list_source cfc_d_list_source cfc_new_list_source cfc_quotient_list_source. ((exists cfc_state_list_sourceprevious. ((exists cfc_left_list_sourcepreviouscode cfc_right_list_sourcepreviouscode cfc_matrix_list_sourcepreviouscode. ((cfc_left_list_sourcepreviouscode = ((cfc_a_list_source) + (cfc_b_list_source)) * S ((cfc_a_list_source) + (cfc_b_list_source)) + ((cfc_b_list_source) + (cfc_b_list_source))) /\ ((cfc_right_list_sourcepreviouscode = ((cfc_c_list_source) + (cfc_d_list_source)) * S ((cfc_c_list_source) + (cfc_d_list_source)) + ((cfc_d_list_source) + (cfc_d_list_source))) /\ ((cfc_matrix_list_sourcepreviouscode = ((cfc_left_list_sourcepreviouscode) + (cfc_right_list_sourcepreviouscode)) * S ((cfc_left_list_sourcepreviouscode) + (cfc_right_list_sourcepreviouscode)) + ((cfc_right_list_sourcepreviouscode) + (cfc_right_list_sourcepreviouscode))) /\ ((cfc_state_list_sourceprevious) = ((cfc_old_list_source) + (cfc_matrix_list_sourcepreviouscode)) * S ((cfc_old_list_source) + (cfc_matrix_list_sourcepreviouscode)) + ((cfc_matrix_list_sourcepreviouscode) + (cfc_matrix_list_sourcepreviouscode))))))) /\ (((exists ff_h_list_sourcepreviousentry. ff_h_list_sourcepreviousentry + S (cfc_state_list_sourceprevious) = S ((S (cfc_index_list_source)) * e)) /\ exists ff_q_list_sourcepreviousentry. h = ff_q_list_sourcepreviousentry * S ((S (cfc_index_list_source)) * e) + (cfc_state_list_sourceprevious))))) /\ ((exists cfc_state_list_sourcefollowing. ((exists cfc_left_list_sourcefollowingcode cfc_right_list_sourcefollowingcode cfc_matrix_list_sourcefollowingcode. ((cfc_left_list_sourcefollowingcode = (((cfc_quotient_list_source * cfc_a_list_source + cfc_c_list_source)) + ((cfc_quotient_list_source * cfc_b_list_source + cfc_d_list_source))) * S (((cfc_quotient_list_source * cfc_a_list_source + cfc_c_list_source)) + ((cfc_quotient_list_source * cfc_b_list_source + cfc_d_list_source))) + (((cfc_quotient_list_source * cfc_b_list_source + cfc_d_list_source)) + ((cfc_quotient_list_source * cfc_b_list_source + cfc_d_list_source)))) /\ ((cfc_right_list_sourcefollowingcode = ((cfc_a_list_source) + (cfc_b_list_source)) * S ((cfc_a_list_source) + (cfc_b_list_source)) + ((cfc_b_list_source) + (cfc_b_list_source))) /\ ((cfc_matrix_list_sourcefollowingcode = ((cfc_left_list_sourcefollowingcode) + (cfc_right_list_sourcefollowingcode)) * S ((cfc_left_list_sourcefollowingcode) + (cfc_right_list_sourcefollowingcode)) + ((cfc_right_list_sourcefollowingcode) + (cfc_right_list_sourcefollowingcode))) /\ ((cfc_state_list_sourcefollowing) = ((cfc_new_list_source) + (cfc_matrix_list_sourcefollowingcode)) * S ((cfc_new_list_source) + (cfc_matrix_list_sourcefollowingcode)) + ((cfc_matrix_list_sourcefollowingcode) + (cfc_matrix_list_sourcefollowingcode))))))) /\ (((exists ff_h_list_sourcefollowingentry. ff_h_list_sourcefollowingentry + S (cfc_state_list_sourcefollowing) = S ((S (S cfc_index_list_source)) * e)) /\ exists ff_q_list_sourcefollowingentry. h = ff_q_list_sourcefollowingentry * S ((S (S cfc_index_list_source)) * e) + (cfc_state_list_sourcefollowing))))) /\ (cfc_new_list_source = S ((cfc_quotient_list_source + cfc_old_list_source) * S (cfc_quotient_list_source + cfc_old_list_source) + (cfc_old_list_source + cfc_old_list_source))))))))) -> (exists cfc_tail_list_target. ((exists cfc_state_list_targetinitial. ((exists cfc_left_list_targetinitialcode cfc_right_list_targetinitialcode cfc_matrix_list_targetinitialcode. ((cfc_left_list_targetinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_list_targetinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_list_targetinitialcode = ((cfc_left_list_targetinitialcode) + (cfc_right_list_targetinitialcode)) * S ((cfc_left_list_targetinitialcode) + (cfc_right_list_targetinitialcode)) + ((cfc_right_list_targetinitialcode) + (cfc_right_list_targetinitialcode))) /\ ((cfc_state_list_targetinitial) = ((cfc_tail_list_target) + (cfc_matrix_list_targetinitialcode)) * S ((cfc_tail_list_target) + (cfc_matrix_list_targetinitialcode)) + ((cfc_matrix_list_targetinitialcode) + (cfc_matrix_list_targetinitialcode))))))) /\ (((exists ff_h_list_targetinitialentry. ff_h_list_targetinitialentry + S (cfc_state_list_targetinitial) = S ((S (0)) * e)) /\ exists ff_q_list_targetinitialentry. h = ff_q_list_targetinitialentry * S ((S (0)) * e) + (cfc_state_list_targetinitial))))) /\ ((exists cfc_state_list_targetterminal. ((exists cfc_left_list_targetterminalcode cfc_right_list_targetterminalcode cfc_matrix_list_targetterminalcode. ((cfc_left_list_targetterminalcode = ((u) + (U)) * S ((u) + (U)) + ((U) + (U))) /\ ((cfc_right_list_targetterminalcode = ((v) + (V)) * S ((v) + (V)) + ((V) + (V))) /\ ((cfc_matrix_list_targetterminalcode = ((cfc_left_list_targetterminalcode) + (cfc_right_list_targetterminalcode)) * S ((cfc_left_list_targetterminalcode) + (cfc_right_list_targetterminalcode)) + ((cfc_right_list_targetterminalcode) + (cfc_right_list_targetterminalcode))) /\ ((cfc_state_list_targetterminal) = ((t) + (cfc_matrix_list_targetterminalcode)) * S ((t) + (cfc_matrix_list_targetterminalcode)) + ((cfc_matrix_list_targetterminalcode) + (cfc_matrix_list_targetterminalcode))))))) /\ (((exists ff_h_list_targetterminalentry. ff_h_list_targetterminalentry + S (cfc_state_list_targetterminal) = S ((S (k)) * e)) /\ exists ff_q_list_targetterminalentry. h = ff_q_list_targetterminalentry * S ((S (k)) * e) + (cfc_state_list_targetterminal))))) /\ (forall cfc_index_list_target. (exists cfba_gap_list_targetbound. cfba_gap_list_targetbound + S (cfc_index_list_target) = (k)) -> exists cfc_old_list_target cfc_a_list_target cfc_b_list_target cfc_c_list_target cfc_d_list_target cfc_new_list_target cfc_quotient_list_target. ((exists cfc_state_list_targetprevious. ((exists cfc_left_list_targetpreviouscode cfc_right_list_targetpreviouscode cfc_matrix_list_targetpreviouscode. ((cfc_left_list_targetpreviouscode = ((cfc_a_list_target) + (cfc_b_list_target)) * S ((cfc_a_list_target) + (cfc_b_list_target)) + ((cfc_b_list_target) + (cfc_b_list_target))) /\ ((cfc_right_list_targetpreviouscode = ((cfc_c_list_target) + (cfc_d_list_target)) * S ((cfc_c_list_target) + (cfc_d_list_target)) + ((cfc_d_list_target) + (cfc_d_list_target))) /\ ((cfc_matrix_list_targetpreviouscode = ((cfc_left_list_targetpreviouscode) + (cfc_right_list_targetpreviouscode)) * S ((cfc_left_list_targetpreviouscode) + (cfc_right_list_targetpreviouscode)) + ((cfc_right_list_targetpreviouscode) + (cfc_right_list_targetpreviouscode))) /\ ((cfc_state_list_targetprevious) = ((cfc_old_list_target) + (cfc_matrix_list_targetpreviouscode)) * S ((cfc_old_list_target) + (cfc_matrix_list_targetpreviouscode)) + ((cfc_matrix_list_targetpreviouscode) + (cfc_matrix_list_targetpreviouscode))))))) /\ (((exists ff_h_list_targetpreviousentry. ff_h_list_targetpreviousentry + S (cfc_state_list_targetprevious) = S ((S (cfc_index_list_target)) * e)) /\ exists ff_q_list_targetpreviousentry. h = ff_q_list_targetpreviousentry * S ((S (cfc_index_list_target)) * e) + (cfc_state_list_targetprevious))))) /\ ((exists cfc_state_list_targetfollowing. ((exists cfc_left_list_targetfollowingcode cfc_right_list_targetfollowingcode cfc_matrix_list_targetfollowingcode. ((cfc_left_list_targetfollowingcode = (((cfc_quotient_list_target * cfc_a_list_target + cfc_c_list_target)) + ((cfc_quotient_list_target * cfc_b_list_target + cfc_d_list_target))) * S (((cfc_quotient_list_target * cfc_a_list_target + cfc_c_list_target)) + ((cfc_quotient_list_target * cfc_b_list_target + cfc_d_list_target))) + (((cfc_quotient_list_target * cfc_b_list_target + cfc_d_list_target)) + ((cfc_quotient_list_target * cfc_b_list_target + cfc_d_list_target)))) /\ ((cfc_right_list_targetfollowingcode = ((cfc_a_list_target) + (cfc_b_list_target)) * S ((cfc_a_list_target) + (cfc_b_list_target)) + ((cfc_b_list_target) + (cfc_b_list_target))) /\ ((cfc_matrix_list_targetfollowingcode = ((cfc_left_list_targetfollowingcode) + (cfc_right_list_targetfollowingcode)) * S ((cfc_left_list_targetfollowingcode) + (cfc_right_list_targetfollowingcode)) + ((cfc_right_list_targetfollowingcode) + (cfc_right_list_targetfollowingcode))) /\ ((cfc_state_list_targetfollowing) = ((cfc_new_list_target) + (cfc_matrix_list_targetfollowingcode)) * S ((cfc_new_list_target) + (cfc_matrix_list_targetfollowingcode)) + ((cfc_matrix_list_targetfollowingcode) + (cfc_matrix_list_targetfollowingcode))))))) /\ (((exists ff_h_list_targetfollowingentry. ff_h_list_targetfollowingentry + S (cfc_state_list_targetfollowing) = S ((S (S cfc_index_list_target)) * e)) /\ exists ff_q_list_targetfollowingentry. h = ff_q_list_targetfollowingentry * S ((S (S cfc_index_list_target)) * e) + (cfc_state_list_targetfollowing))))) /\ (cfc_new_list_target = S ((cfc_quotient_list_target + cfc_old_list_target) * S (cfc_quotient_list_target + cfc_old_list_target) + (cfc_old_list_target + cfc_old_list_target)))))))))Constructive proof overview
Generated structural guide
Equality of actual tagged quotient lists transports the finite computation by ordinary substitution.
The unchanged tactic script uses 0 declared prerequisites and contains 14 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
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
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–10
02Fix variables and assumptionsL11–11
Work with arbitrary variables or the premises of the current implication.
- L11
intro ht
03Calculate and transport equalitiesL12–13
04Use earlier factsL14–14
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L14
exact ht