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
ScaledInverseIndex(m,t,l,i,y)Exact expansion
((exists dp_index_gap. dp_index_gap + S i = l) /\ ((((~((S i) = 0) /\ (exists dp_gap. dp_gap + S (S i) = m))) /\ (((~((y) = 0) /\ (exists dp_gap. dp_gap + S (y) = m))) /\ (exists dp_u dp_v. (S i) * (y) + m * dp_u = (t) + 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
Used by theorem statements or local proof propositions
PA008R prime_scaled_inverse_prefix_extend PA0099 scaled_inverse_prefix_entry_sound PA009A scaled_inverse_prefix_mate_predecessor PA009D scaled_inverse_prefix_extensional PA009E scaled_inverse_prefix_involutive PA009H scaled_inverse_prefix_no_fixed_of_not_qres PA009I scaled_inverse_prefix_choose_omitted_orbit PA009X scaled_pair_order_successor_lift_adjacent_targets