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
ScaledInversePrefix(m,t,l,b,c,k)Exact expansion
forall dp_i. (exists dp_prefix_gap. dp_prefix_gap + S dp_i = k) -> exists dp_y. ((((exists ff_h_defined_scaled_inverse_prefix_entry. ff_h_defined_scaled_inverse_prefix_entry + S (dp_y) = S ((S (dp_i)) * c)) /\ exists ff_q_defined_scaled_inverse_prefix_entry. b = ff_q_defined_scaled_inverse_prefix_entry * S ((S (dp_i)) * c) + (dp_y))) /\ (((exists dp_index_gap. dp_index_gap + S dp_i = l) /\ ((((~((S dp_i) = 0) /\ (exists dp_gap. dp_gap + S (S dp_i) = m))) /\ (((~((dp_y) = 0) /\ (exists dp_gap. dp_gap + S (dp_y) = m))) /\ (exists dp_u dp_v. (S dp_i) * (dp_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
none
Used by theorem statements or local proof propositions
PA008R prime_scaled_inverse_prefix_extend PA008S prime_scaled_inverse_prefix_exists_bounded PA008T prime_scaled_inverse_prefix_exists 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 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 PA009X scaled_pair_order_successor_lift_adjacent_targets PA00BK scaled_pair_order_terminal_power_mod_predecessor PA00BL scaled_inverse_nonresidue_half_power_mod_predecessor PA00BM quadratic_nonresidue_half_power_mod_predecessor