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
Repeat(b,c,a,l)Exact expansion
forall ff_i_defined_repeat. (exists ff_lt_defined_repeat_bound. ff_lt_defined_repeat_bound + S ff_i_defined_repeat = l) -> (((exists ff_h_defined_repeat_decoded. ff_h_defined_repeat_decoded + S (a) = S ((S (ff_i_defined_repeat)) * c)) /\ exists ff_q_defined_repeat_decoded. b = ff_q_defined_repeat_decoded * S ((S (ff_i_defined_repeat)) * c) + (a)))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
PA0043 beta_repeat_empty PA0044 beta_repeat_succ_extend PA0045 beta_repeat_exists PA0046 pow_exists PA004C beta_repeat_entry_eq PA005F beta_repeat_transport_entry PA00BW beta_scaled_successor_prefix_from_pointwise PA00C0 prime_scaled_half_division_prefix_exists PA00DW beta_all_one_bit_count_exact PA00DX eisenstein_initial_segment_bit_count_functional PA00EK beta_repeat_sum_exact PA00EL beta_repeat_sum_exists_exact PA00EO eisenstein_transposed_column_count_matches_decoded_constant PA00EQ eisenstein_rectangle_plus_column_count_total PA00ES eisenstein_zero_width_rectangle_sum_zero