BoundedPrefix

Readable signature

BoundedPrefix(b, c, l)

Exact expansion

forall fp_i_defined_bounded_prefix. (exists fp_gap_defined_bounded_prefix_index. fp_gap_defined_bounded_prefix_index + S fp_i_defined_bounded_prefix = l) -> exists fp_value_defined_bounded_prefix. ((((exists ff_h_defined_bounded_prefix_entry. ff_h_defined_bounded_prefix_entry + S (fp_value_defined_bounded_prefix) = S ((S (fp_i_defined_bounded_prefix)) * c)) /\ exists ff_q_defined_bounded_prefix_entry. b = ff_q_defined_bounded_prefix_entry * S ((S (fp_i_defined_bounded_prefix)) * c) + (fp_value_defined_bounded_prefix))) /\ (exists fp_gap_defined_bounded_prefix_value. fp_gap_defined_bounded_prefix_value + S fp_value_defined_bounded_prefix = l))

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

Used by conservative definitions

All transitive conservative prerequisites

Used by theorem statements or local proof propositions

Grand-campaign planning vocabulary

Locate BoundedPrefix in the global campaign vocabulary →

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

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.