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
ContainsPrefix(b,c,l,x)Exact expansion
exists fp_i_defined_contains_prefix. ((exists fp_gap_defined_contains_prefix_index. fp_gap_defined_contains_prefix_index + S fp_i_defined_contains_prefix = l) /\ (((exists ff_h_defined_contains_prefix_entry. ff_h_defined_contains_prefix_entry + S (x) = S ((S (fp_i_defined_contains_prefix)) * c)) /\ exists ff_q_defined_contains_prefix_entry. b = ff_q_defined_contains_prefix_entry * S ((S (fp_i_defined_contains_prefix)) * c) + (x))))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
PA004H finite_contains_decidable PA004R finite_last_is_top_from_prefix_surjective PA004S finite_surjective_succ_intro PA004U finite_swap_last_surjective_back PA004V finite_no_top_successor_gate PA004W finite_bounded_injective_surjective PA007X beta_product_permutation_invariant PA008U scaled_orbit_closed_prefix_zero PA008X scaled_pair_order_state_zero PA0092 finite_covers_into_or_omits PA0093 finite_inverse_choice_prefix_extend PA0094 finite_inverse_choice_prefix_exists PA0097 finite_short_cover_impossible PA0098 finite_short_prefix_omits PA009I scaled_inverse_prefix_choose_omitted_orbit PA009J scaled_orbit_closed_unused_mate PA009M beta_prefix_append_two_scaled_orbit_closed PA009N beta_prefix_append_two_injective PA009O scaled_inverse_pair_order_choose_append PA009T scaled_inverse_pair_order_paired_state_step PA009V scaled_inverse_pair_order_paired_iteration PA009W scaled_inverse_pair_order_terminal_package PA00A8 orbit_closed_prefix_zero PA00AA pair_order_state_zero PA00AE finite_prefix_choose_unused_nonendpoint PA00AR prime_choose_unused_nonendpoint_orbit PA00AS orbit_closed_unused_mate PA00AT beta_prefix_append_two_orbit_closed PA00AV prime_pair_order_choose_append PA00AW prime_pair_order_choose_append_injective PA00AX prime_pair_order_choose_append_state PA00B0 prime_pair_order_paired_state_step PA00B1 prime_pair_order_paired_iteration PA00B2 prime_pair_order_paired_terminal_state_exists PA00B4 finite_bounded_nonendpoint_injective_coverage PA00B5 pair_order_state_terminal_coverage PA00BB pair_order_terminal_state_magnitude_range PA00BE prime_wilson_terminal_product_package_exists PA00BF prime_terminal_range_two_product_mod_one_exists PA00BK scaled_pair_order_terminal_power_mod_predecessor PA00BL scaled_inverse_nonresidue_half_power_mod_predecessor PA00CX beta_sum_permutation_invariant