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
InversePrefix(m,l,b,c,k)Exact expansion
forall dp_i. (exists dp_prefix_gap. dp_prefix_gap + S dp_i = k) -> exists dp_j. ((((exists ff_h_defined_inverse_prefix_entry. ff_h_defined_inverse_prefix_entry + S (dp_j) = S ((S (dp_i)) * c)) /\ exists ff_q_defined_inverse_prefix_entry. b = ff_q_defined_inverse_prefix_entry * S ((S (dp_i)) * c) + (dp_j))) /\ (((exists dp_left_gap. dp_left_gap + S dp_i = l) /\ ((exists dp_right_gap. dp_right_gap + S dp_j = l) /\ (exists dp_u dp_v. (S dp_i) * S dp_j + m * dp_u = 1 + m * dp_v)))))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
PA00A5 prime_inverse_prefix_extend PA00A6 prime_inverse_prefix_exists_bounded PA00A7 prime_inverse_prefix_exists PA00AF inverse_prefix_entry_sound PA00AH prime_inverse_prefix_fixed_cases PA00AI prime_inverse_prefix_nonendpoint_not_fixed PA00AM inverse_prefix_extensional PA00AN inverse_prefix_involutive PA00AO inverse_prefix_zero_fixed PA00AP inverse_prefix_last_fixed PA00AQ prime_inverse_prefix_nonendpoint_mate PA00AR prime_choose_unused_nonendpoint_orbit 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 PA00B7 paired_successor_lift_adjacent_units PA00B8 paired_pair_order_factor_code_exists PA00BA paired_pair_order_product_one_exists PA00BE prime_wilson_terminal_product_package_exists PA00BF prime_terminal_range_two_product_mod_one_exists