SurjectivePrefix

Readable signature

SurjectivePrefix(b, c, l)

Exact expansion

forall fp_value_defined_surjective_prefix. (exists fp_gap_defined_surjective_prefix_value. fp_gap_defined_surjective_prefix_value + S fp_value_defined_surjective_prefix = l) -> exists fp_i_defined_surjective_prefix. ((exists fp_gap_defined_surjective_prefix_index. fp_gap_defined_surjective_prefix_index + S fp_i_defined_surjective_prefix = l) /\ (((exists ff_h_defined_surjective_prefix_entry. ff_h_defined_surjective_prefix_entry + S (fp_value_defined_surjective_prefix) = S ((S (fp_i_defined_surjective_prefix)) * c)) /\ exists ff_q_defined_surjective_prefix_entry. b = ff_q_defined_surjective_prefix_entry * S ((S (fp_i_defined_surjective_prefix)) * c) + (fp_value_defined_surjective_prefix))))

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 SurjectivePrefix in the global campaign vocabulary →

Reviewed SurjectivePrefix corresponds to blueprint SurjectivePrefix 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.