PD0018 · conservative definition

Range

The decoded prefix is a,a+1,...,a+l-1.

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 conservative notation, not a theorem, axiom, predicate constant, or kernel rule. Its expansion remains in the unchanged first-order language.

Definition neighborhood

Depends on conservative definitions

PD0002 Lt PD0013 BetaAt

Used by conservative definitions

none

All transitive conservative prerequisites

PD0002 Lt PD0013 BetaAt

Used by theorem statements or local proof propositions

SL0007 bounded_gauss_lemma_complete SL000K doubling_gauss_initial_segment_complement SL000N doubling_gauss_reflection_count_shape SL000Q quadratic_supplement_two_half_complete

Grand-campaign planning vocabulary

Locate Range in the global campaign vocabulary →

Reviewed Range corresponds to blueprint Range with checked argument positions [0, 1, 2, 3].

The global atlas describes planning vocabulary and does not itself certify a definition or theorem. The reviewed expansion and conservative dependency DAG on this page are the actual family-local reading definitions.