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
InjectivePrefix(b,c,l)Exact expansion
forall fp_i_defined_injective_prefix fp_j_defined_injective_prefix fp_value_defined_injective_prefix. (exists fp_gap_defined_injective_prefix_i. fp_gap_defined_injective_prefix_i + S fp_i_defined_injective_prefix = l) -> (exists fp_gap_defined_injective_prefix_j. fp_gap_defined_injective_prefix_j + S fp_j_defined_injective_prefix = l) -> (((exists ff_h_defined_injective_prefix_left. ff_h_defined_injective_prefix_left + S (fp_value_defined_injective_prefix) = S ((S (fp_i_defined_injective_prefix)) * c)) /\ exists ff_q_defined_injective_prefix_left. b = ff_q_defined_injective_prefix_left * S ((S (fp_i_defined_injective_prefix)) * c) + (fp_value_defined_injective_prefix))) -> (((exists ff_h_defined_injective_prefix_right. ff_h_defined_injective_prefix_right + S (fp_value_defined_injective_prefix) = S ((S (fp_j_defined_injective_prefix)) * c)) /\ exists ff_q_defined_injective_prefix_right. b = ff_q_defined_injective_prefix_right * S ((S (fp_j_defined_injective_prefix)) * c) + (fp_value_defined_injective_prefix))) -> fp_i_defined_injective_prefix = fp_j_defined_injective_prefixThis 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
PA004O finite_swap_last_injective PA004Q finite_injective_prefix_succ 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 PA007C gauss_signed_half_magnitude_injective PA007U beta_magnitude_predecessor_recode_injective PA007X beta_product_permutation_invariant PA007Y gauss_magnitude_product_eq_half_range PA0080 gauss_signed_products_balance_mod PA0084 gauss_signed_products_cancel_mod PA0085 gauss_lemma_power_congruence_exists PA008E prime_mul_index_map_injective PA008I prime_mul_residue_reindex_exists PA008J prime_mul_residue_product_balance PA008W injective_prefix_zero PA008X scaled_pair_order_state_zero PA0096 finite_inverse_choice_injective PA0097 finite_short_cover_impossible 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 PA00A1 scaled_pair_order_successor_lift_product_is_factorial PA00AA pair_order_state_zero 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 PA00B3 beta_magnitude_predecessor_recode_surjective PA00B4 finite_bounded_nonendpoint_injective_coverage PA00B5 pair_order_state_terminal_coverage PA00BB pair_order_terminal_state_magnitude_range PA00BD pair_order_terminal_successor_product_eq_range_two 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 PA00CY beta_magnitude_sum_permutation_exact PA00D0 gauss_signed_half_magnitude_sum_equals_half_sum