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
Range(b,c,a,l)Exact expansion
forall ff_i_defined_range. (exists ff_lt_defined_range_bound. ff_lt_defined_range_bound + S ff_i_defined_range = l) -> (((exists ff_h_defined_range_decoded. ff_h_defined_range_decoded + S (a + ff_i_defined_range) = S ((S (ff_i_defined_range)) * c)) /\ exists ff_q_defined_range_decoded. b = ff_q_defined_range_decoded * S ((S (ff_i_defined_range)) * c) + (a + ff_i_defined_range)))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
PA0006 beta_range_empty PA002Y beta_range_succ_extend PA0030 beta_range_exists PA0032 beta_range_entry_eq PA0034 beta_half_range_entry_bounds PA003T beta_range_injective PA0060 factorial_exists PA006A beta_range_transport_entry PA0072 gauss_half_range_signed_choices PA0075 gauss_half_range_signed_prefix_exists PA007C gauss_signed_half_magnitude_injective PA007V gauss_predecessor_half_range_aligned PA007Y gauss_magnitude_product_eq_half_range PA0080 gauss_signed_products_balance_mod PA0083 prime_half_range_product_coprime PA0084 gauss_signed_products_cancel_mod PA0085 gauss_lemma_power_congruence_exists PA008F beta_range_one_entry_eq_succ PA008G beta_successor_range_reindex_aligned PA008H beta_successor_range_scale_mod PA008I prime_mul_residue_reindex_exists PA008J prime_mul_residue_product_balance PA008K prime_range_product_coprime PA00BC pair_order_predecessor_range_two_successor_lift_aligned 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 PA00BG beta_range_two_product_is_factorial_succ PA00BH beta_range_two_product_restore_last PA00BJ prime_factorial_wilson_congruence PA00BV arbitrary_gauss_lemma_complete PA00BW beta_scaled_successor_prefix_from_pointwise PA00C0 prime_scaled_half_division_prefix_exists PA00C1 prime_scaled_half_quotient_sum_exists PA00CP gauss_eisenstein_prefix_pointwise_mod_two PA00CR gauss_eisenstein_terminal_sums_mod_two PA00CS beta_magnitude_predecessor_recode_aligned_half_range PA00CY beta_magnitude_sum_permutation_exact PA00D0 gauss_signed_half_magnitude_sum_equals_half_sum PA00D3 gauss_eisenstein_terminal_cancel_magnitude_mod_two PA00D6 gauss_eisenstein_sign_count_mod_quotient_sum PA00D7 odd_prime_gauss_eisenstein_orientation_data_exists