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.
Readable signature
BoundedPrefix(b,c,l)Exact expansion
forall fp_i_defined_bounded_prefix. (exists fp_gap_defined_bounded_prefix_index. fp_gap_defined_bounded_prefix_index + S fp_i_defined_bounded_prefix = l) -> exists fp_value_defined_bounded_prefix. ((((exists ff_h_defined_bounded_prefix_entry. ff_h_defined_bounded_prefix_entry + S (fp_value_defined_bounded_prefix) = S ((S (fp_i_defined_bounded_prefix)) * c)) /\ exists ff_q_defined_bounded_prefix_entry. b = ff_q_defined_bounded_prefix_entry * S ((S (fp_i_defined_bounded_prefix)) * c) + (fp_value_defined_bounded_prefix))) /\ (exists fp_gap_defined_bounded_prefix_value. fp_gap_defined_bounded_prefix_value + S fp_value_defined_bounded_prefix = l))This node is notation, not a theorem, axiom, predicate constant, or kernel rule. The elaboration layer must expand it before proof checking.
Definition neighborhood
Expands using
Used by definitions
none
Used by theorem statements or local proof propositions
PA004I finite_bounded_last_succ PA004L finite_bounded_entry_lt PA004M finite_swap_last_bounded PA004P finite_bounded_prefix_without_top PA004R finite_last_is_top_from_prefix_surjective PA004T finite_surjective_succ_from_prefix PA004V finite_no_top_successor_gate PA004W finite_bounded_injective_surjective PA004X finite_fixed_last_prefix_bounded PA007S beta_magnitude_predecessor_recode_bounded PA007V gauss_predecessor_half_range_aligned PA007X beta_product_permutation_invariant PA007Y gauss_magnitude_product_eq_half_range PA008D fermat_index_map_bounded PA008G beta_successor_range_reindex_aligned PA008I prime_mul_residue_reindex_exists PA008J prime_mul_residue_product_balance PA0097 finite_short_cover_impossible PA00A1 scaled_pair_order_successor_lift_product_is_factorial PA00B3 beta_magnitude_predecessor_recode_surjective PA00BC pair_order_predecessor_range_two_successor_lift_aligned PA00BD pair_order_terminal_successor_product_eq_range_two PA00BK scaled_pair_order_terminal_power_mod_predecessor PA00CX beta_sum_permutation_invariant PA00CY beta_magnitude_sum_permutation_exact