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 a b c l. (forall bpr_index_bpfpra_source. (exists bpr_gap_bpfpra_source_bound. bpr_gap_bpfpra_source_bound + S (bpr_index_bpfpra_source) = a + l) -> exists bpr_value_bpfpra_source. ((((exists bpr_height_bpfpra_source_decoded. bpr_height_bpfpra_source_decoded + S (bpr_value_bpfpra_source) = S ((S (bpr_index_bpfpra_source)) * c)) /\ exists bpr_quotient_bpfpra_source_decoded. b = bpr_quotient_bpfpra_source_decoded * S ((S (bpr_index_bpfpra_source)) * c) + (bpr_value_bpfpra_source))) /\ (((((~(S (bpr_index_bpfpra_source) = 1) /\ forall bpr_left_bpfpra_source_choice_prime bpr_right_bpfpra_source_choice_prime. S (bpr_index_bpfpra_source) = bpr_left_bpfpra_source_choice_prime * bpr_right_bpfpra_source_choice_prime -> bpr_left_bpfpra_source_choice_prime = 1 \/ bpr_right_bpfpra_source_choice_prime = 1)) /\ bpr_value_bpfpra_source = S (bpr_index_bpfpra_source)) \/ (~((~(S (bpr_index_bpfpra_source) = 1) /\ forall bpr_left_bpfpra_source_choice_prime bpr_right_bpfpra_source_choice_prime. S (bpr_index_bpfpra_source) = bpr_left_bpfpra_source_choice_prime * bpr_right_bpfpra_source_choice_prime -> bpr_left_bpfpra_source_choice_prime = 1 \/ bpr_right_bpfpra_source_choice_prime = 1)) /\ bpr_value_bpfpra_source = 1))))) -> (forall bpr_index_bpfpra_target. (exists bpr_gap_bpfpra_target_bound. bpr_gap_bpfpra_target_bound + S (bpr_index_bpfpra_target) = a) -> exists bpr_value_bpfpra_target. ((((exists bpr_height_bpfpra_target_decoded. bpr_height_bpfpra_target_decoded + S (bpr_value_bpfpra_target) = S ((S (bpr_index_bpfpra_target)) * c)) /\ exists bpr_quotient_bpfpra_target_decoded. b = bpr_quotient_bpfpra_target_decoded * S ((S (bpr_index_bpfpra_target)) * c) + (bpr_value_bpfpra_target))) /\ (((((~(S (bpr_index_bpfpra_target) = 1) /\ forall bpr_left_bpfpra_target_choice_prime bpr_right_bpfpra_target_choice_prime. S (bpr_index_bpfpra_target) = bpr_left_bpfpra_target_choice_prime * bpr_right_bpfpra_target_choice_prime -> bpr_left_bpfpra_target_choice_prime = 1 \/ bpr_right_bpfpra_target_choice_prime = 1)) /\ bpr_value_bpfpra_target = S (bpr_index_bpfpra_target)) \/ (~((~(S (bpr_index_bpfpra_target) = 1) /\ forall bpr_left_bpfpra_target_choice_prime bpr_right_bpfpra_target_choice_prime. S (bpr_index_bpfpra_target) = bpr_left_bpfpra_target_choice_prime * bpr_right_bpfpra_target_choice_prime -> bpr_left_bpfpra_target_choice_prime = 1 \/ bpr_right_bpfpra_target_choice_prime = 1)) /\ bpr_value_bpfpra_target = 1)))))Structural proof guide
Restrict a selector prefix of length a+l to its first a entries.
Direct prerequisites: le_add_right, lt_of_lt_of_le. 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.
Named ingredients (2)
01Fix variables and assumptionsL1–7
02Use earlier factsL8–16
Instantiate or apply named facts and discharge the corresponding proof obligations.
Original exact command ledger · 16 lines
- 0001
intro a - 0002
intro b - 0003
intro c - 0004
intro l - 0005
intro hsource - 0006
intro i - 0007
intro hi - 0008
apply hsource - 0009
specialize lt_of_lt_of_le i - 0010
specialize lt_of_lt_of_le a - 0011
specialize lt_of_lt_of_le (a + l) - 0012
apply lt_of_lt_of_le - 0013
exact hi - 0014
specialize le_add_right a - 0015
specialize le_add_right l - 0016
exact le_add_right