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 conservative notation, not a theorem, new axiom, predicate constant, or kernel rule. Its expansion is checked for exact first-order AST equivalence.
Definition neighborhood
Expands using
Used by definitions
Used by theorem statements or local proof propositions
BT007U beta_repeat_empty BT007V beta_repeat_succ_extend BT007W beta_repeat_exists BT007X beta_repeat_entry_eq BT007Y beta_repeat_transport_entry BT0080 pow_exists BT00JC beta_all_one_bit_count_exact BT00JD eisenstein_initial_segment_bit_count_functional BT00YC double_quotient_carry_prefix_entries_zero BT00YD central_binom_prime_valuation_zero_of_exact_double_quotients