InjectivePrefix

Readable signature

InjectivePrefix(b, c, l)

Exact expansion

forall fp_i_defined_injective_prefix fp_j_defined_injective_prefix fp_value_defined_injective_prefix. (exists fp_gap_defined_injective_prefix_i. fp_gap_defined_injective_prefix_i + S fp_i_defined_injective_prefix = l) -> (exists fp_gap_defined_injective_prefix_j. fp_gap_defined_injective_prefix_j + S fp_j_defined_injective_prefix = l) -> (((exists ff_h_defined_injective_prefix_left. ff_h_defined_injective_prefix_left + S (fp_value_defined_injective_prefix) = S ((S (fp_i_defined_injective_prefix)) * c)) /\ exists ff_q_defined_injective_prefix_left. b = ff_q_defined_injective_prefix_left * S ((S (fp_i_defined_injective_prefix)) * c) + (fp_value_defined_injective_prefix))) -> (((exists ff_h_defined_injective_prefix_right. ff_h_defined_injective_prefix_right + S (fp_value_defined_injective_prefix) = S ((S (fp_j_defined_injective_prefix)) * c)) /\ exists ff_q_defined_injective_prefix_right. b = ff_q_defined_injective_prefix_right * S ((S (fp_j_defined_injective_prefix)) * c) + (fp_value_defined_injective_prefix))) -> fp_i_defined_injective_prefix = fp_j_defined_injective_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 InjectivePrefix in the global campaign vocabulary →

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