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 PA statement
forall b c d e f g l. (forall b5cc_index_b5ccpr_source. (exists bcf_lt_gap_b5ccpr_source_bound. bcf_lt_gap_b5ccpr_source_bound + S (b5cc_index_b5ccpr_source) = S l) -> exists b5cc_left_b5ccpr_source b5cc_right_b5ccpr_source b5cc_bit_b5ccpr_source. (((exists fs_h_b5cc_b5ccpr_source_left. fs_h_b5cc_b5ccpr_source_left + S (b5cc_left_b5ccpr_source) = S ((S (b5cc_index_b5ccpr_source)) * c)) /\ exists fs_q_b5cc_b5ccpr_source_left. b = fs_q_b5cc_b5ccpr_source_left * S ((S (b5cc_index_b5ccpr_source)) * c) + (b5cc_left_b5ccpr_source))) /\ ((((exists fs_h_b5cc_b5ccpr_source_right. fs_h_b5cc_b5ccpr_source_right + S (b5cc_right_b5ccpr_source) = S ((S (b5cc_index_b5ccpr_source)) * e)) /\ exists fs_q_b5cc_b5ccpr_source_right. d = fs_q_b5cc_b5ccpr_source_right * S ((S (b5cc_index_b5ccpr_source)) * e) + (b5cc_right_b5ccpr_source))) /\ ((((exists fs_h_b5cc_b5ccpr_source_bit. fs_h_b5cc_b5ccpr_source_bit + S (b5cc_bit_b5ccpr_source) = S ((S (b5cc_index_b5ccpr_source)) * g)) /\ exists fs_q_b5cc_b5ccpr_source_bit. f = fs_q_b5cc_b5ccpr_source_bit * S ((S (b5cc_index_b5ccpr_source)) * g) + (b5cc_bit_b5ccpr_source))) /\ (((b5cc_bit_b5ccpr_source = 0 /\ b5cc_right_b5ccpr_source = b5cc_left_b5ccpr_source + b5cc_left_b5ccpr_source) \/ (b5cc_bit_b5ccpr_source = 1 /\ b5cc_right_b5ccpr_source = S (b5cc_left_b5ccpr_source + b5cc_left_b5ccpr_source))))))) -> (forall b5cc_index_b5ccpr_result. (exists bcf_lt_gap_b5ccpr_result_bound. bcf_lt_gap_b5ccpr_result_bound + S (b5cc_index_b5ccpr_result) = l) -> exists b5cc_left_b5ccpr_result b5cc_right_b5ccpr_result b5cc_bit_b5ccpr_result. (((exists fs_h_b5cc_b5ccpr_result_left. fs_h_b5cc_b5ccpr_result_left + S (b5cc_left_b5ccpr_result) = S ((S (b5cc_index_b5ccpr_result)) * c)) /\ exists fs_q_b5cc_b5ccpr_result_left. b = fs_q_b5cc_b5ccpr_result_left * S ((S (b5cc_index_b5ccpr_result)) * c) + (b5cc_left_b5ccpr_result))) /\ ((((exists fs_h_b5cc_b5ccpr_result_right. fs_h_b5cc_b5ccpr_result_right + S (b5cc_right_b5ccpr_result) = S ((S (b5cc_index_b5ccpr_result)) * e)) /\ exists fs_q_b5cc_b5ccpr_result_right. d = fs_q_b5cc_b5ccpr_result_right * S ((S (b5cc_index_b5ccpr_result)) * e) + (b5cc_right_b5ccpr_result))) /\ ((((exists fs_h_b5cc_b5ccpr_result_bit. fs_h_b5cc_b5ccpr_result_bit + S (b5cc_bit_b5ccpr_result) = S ((S (b5cc_index_b5ccpr_result)) * g)) /\ exists fs_q_b5cc_b5ccpr_result_bit. f = fs_q_b5cc_b5ccpr_result_bit * S ((S (b5cc_index_b5ccpr_result)) * g) + (b5cc_bit_b5ccpr_result))) /\ (((b5cc_bit_b5ccpr_result = 0 /\ b5cc_right_b5ccpr_result = b5cc_left_b5ccpr_result + b5cc_left_b5ccpr_result) \/ (b5cc_bit_b5ccpr_result = 1 /\ b5cc_right_b5ccpr_result = S (b5cc_left_b5ccpr_result + b5cc_left_b5ccpr_result)))))))Structural proof guide
Dropping the final position preserves a carry prefix.
Direct prerequisites: le_succ. The authored body proceeds by direct introduction and elimination.
Proof neighborhood
Direct dependencies
Direct dependents
Formal native tactic body
Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing 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.