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
SurjectivePrefix(b,c,l)Exact expansion
forall fp_value_defined_surjective_prefix. (exists fp_gap_defined_surjective_prefix_value. fp_gap_defined_surjective_prefix_value + S fp_value_defined_surjective_prefix = l) -> exists fp_i_defined_surjective_prefix. ((exists fp_gap_defined_surjective_prefix_index. fp_gap_defined_surjective_prefix_index + S fp_i_defined_surjective_prefix = l) /\ (((exists ff_h_defined_surjective_prefix_entry. ff_h_defined_surjective_prefix_entry + S (fp_value_defined_surjective_prefix) = S ((S (fp_i_defined_surjective_prefix)) * c)) /\ exists ff_q_defined_surjective_prefix_entry. b = ff_q_defined_surjective_prefix_entry * S ((S (fp_i_defined_surjective_prefix)) * c) + (fp_value_defined_surjective_prefix))))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
PA004F finite_surjective_zero PA004R finite_last_is_top_from_prefix_surjective PA004S finite_surjective_succ_intro PA004T finite_surjective_succ_from_prefix PA004U finite_swap_last_surjective_back PA004V finite_no_top_successor_gate PA004W finite_bounded_injective_surjective PA007X beta_product_permutation_invariant PA0097 finite_short_cover_impossible PA00B3 beta_magnitude_predecessor_recode_surjective PA00B4 finite_bounded_nonendpoint_injective_coverage PA00CX beta_sum_permutation_invariant